Commit 2026-03-06 21:32 aae3b08d

View on Github →

feat(FieldTheory/RatFunc): Lüroth's theorem (#36109)

Estimated changes

Modified Mathlib/FieldTheory/RatFunc/Luroth.lean

added theorem RatFunc.IntermediateField.isAlgebraic_X

added theorem RatFunc.Luroth.C_c_mul_φ

added theorem RatFunc.Luroth.Q₀_mem_lifts

added theorem RatFunc.Luroth.Q₀_mul_Φ

added theorem RatFunc.Luroth.Q₀_ne_zero

added theorem RatFunc.Luroth.Q₁_mul_Φ

added theorem RatFunc.Luroth.Q₁_ne_zero

added theorem RatFunc.Luroth.Q₂_map

added theorem RatFunc.Luroth.Q₂_mul_Φ

added theorem RatFunc.Luroth.Q₂_natDegree

added theorem RatFunc.Luroth.Q₂_ne_zero

added theorem RatFunc.Luroth.Q₃_map

added theorem RatFunc.Luroth.Q₃_mul_Φ

added def RatFunc.Luroth.b

added theorem RatFunc.Luroth.b_ne_zero

added theorem RatFunc.Luroth.c_denom

added theorem RatFunc.Luroth.c_ne_zero

added theorem RatFunc.Luroth.exists_φ_coeff_not_mem

added def RatFunc.Luroth.generatorIndex

added theorem RatFunc.Luroth.generator_denom_dvd_c_num

added theorem RatFunc.Luroth.generator_eq_coeff

added theorem RatFunc.Luroth.le_Φ_coeff_generatorIndex_natDegree

added theorem RatFunc.Luroth.le_Φ_coeff_natDegree_natDegree

added theorem RatFunc.Luroth.m_le_swap_Φ_natDegree

added theorem RatFunc.Luroth.map_Q₁

added theorem RatFunc.Luroth.q_ne_zero

added theorem RatFunc.Luroth.swap_Q₁_natDegree

added theorem RatFunc.Luroth.swap_Φ_natDegree_eq_θ_natDegree

added theorem RatFunc.Luroth.swap_θ

added theorem RatFunc.Luroth.Φ'_map

added theorem RatFunc.Luroth.Φ'_ne_zero

added theorem RatFunc.Luroth.Φ_coeff_generatorIndex

added theorem RatFunc.Luroth.Φ_coeff_generatorIndex_ne_zero

added theorem RatFunc.Luroth.Φ_coeff_φ_natDegree'

added theorem RatFunc.Luroth.Φ_coeff_φ_natDegree

added theorem RatFunc.Luroth.Φ_coeff_φ_natDegree_ne_zero

added theorem RatFunc.Luroth.Φ_natDegree_eq_θ_natDegree

added theorem RatFunc.Luroth.Φ_natDegree_eq_φ_natDegree

added theorem RatFunc.Luroth.Φ_ne_zero

added theorem RatFunc.Luroth.θ_natDegree_le

added theorem RatFunc.Luroth.φ_dvd_generator_minpolyX

added theorem RatFunc.Luroth.φ_monic

added theorem RatFunc.Luroth.φ_mul_q

added theorem RatFunc.Luroth.φ_natDegree

added theorem RatFunc.Luroth.φ_ne_zero

Modified Mathlib/RingTheory/Coprime/Basic.lean

added theorem IsCoprime.isUnit_of_associated

Modified docs/references.bib