Module

RationalFunctionNonsquare.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Arithmetic.RationalFunctionNonsquare

1 declaration indexed from sourceView source ↗

Module documentation

A linear polynomial is not a square in the rational function field

The discriminant in Proposition 2.5 of Shimizu--Yamaguchi has degree one. Its nonsquareness follows from the integer degree of rational functions: a nonzero square has even degree. This argument does not require a choice of a root or an algebraic closure.

Source: Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers, Proposition 2.5.

Imports3

Mathlib.Algebra.Polynomial.Degree.SmallDegree
Mathlib.FieldTheory.RatFunc.Degree
Lean.Elab.Tactic.Omega

Imported by2

theorem

linearPolynomial_ne_square_ratFunc

L31 ↗

ShimizuYamaguchi26BranchedCoverings.linearPolynomial_ne_square_ratFunc

Documentation

A nonconstant linear polynomial is not the square of a rational function.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoverings

Lean source · statement

theorem linearPolynomial_ne_square_ratFunc {K : Type*} [Field K]
    (a b : K) (ha : a ≠ 0) (r : RatFunc K) :
    algebraMap K[X] (RatFunc K) (C a * X + C b) ≠ r ^ 2

Module documentation

A linear polynomial is not a square in the rational function field

Declarations

linearPolynomial_ne_square_ratFunc