RepeatedRoot.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The algebraic obstruction to exceptional returns

EKL (Annals of Mathematics 164 (2006), Proposition 5.2) excludes an integral special-linear matrix with exactly one repeated eigenvalue and no eigenvalues equal to ±1. The first step is that a unique repeated root of a rational polynomial must be rational: a distinct Galois conjugate would also be a common root of the polynomial and its derivative.

theorem OAI.DukePrimeDegree.unique_common_root_is_rational line 23
theorem OAI.DukePrimeDegree.rational_root_of_monic_unit_constant line 43

theorem OAI.DukePrimeDegree.unique_common_root_of_monic_unit_constant line 59

Source documentation

The repeated-root obstruction in EKL Proposition 5.2, in polynomial form.

theorem unique_common_root_of_monic_unit_constant
    (p : ℤ[X]) (hp : p.Monic) (hc : IsUnit (p.coeff 0)) (x : ℂ)
    (hx : aeval x p = 0) (hdx : aeval x p.derivative = 0)
    (hunique : ∀ y : ℂ, aeval y p = 0 → aeval y p.derivative = 0 → y = x) :
    x = 1 ∨ x = -1 := by
…

theorem OAI.DukePrimeDegree.unique_repeated_root_of_monic_unit_constant line 98

Source documentation

A unique multiple complex root of a monic integer unit polynomial must be one of the two rational units.

theorem unique_repeated_root_of_monic_unit_constant
    (p : ℤ[X]) (hp : p.Monic) (hc : IsUnit (p.coeff 0)) (x : ℂ)
    (hx : 1 < (p.map (algebraMap ℤ ℂ)).rootMultiplicity x)
    (hunique : ∀ y : ℂ, 1 < (p.map (algebraMap ℤ ℂ)).rootMultiplicity y → y = x) :
    x = 1 ∨ x = -1 := by
…

theorem OAI.DukePrimeDegree.integer_sl_unique_repeated_root line 120

Source documentation

Polynomial form of EKL Proposition 5.2 for integral special-linear matrices.

theorem integer_sl_unique_repeated_root {n : ℕ}
    (g : Matrix.SpecialLinearGroup (Fin n) ℤ) (x : ℂ)
    (hx : 1 < (g.val.charpoly.map (algebraMap ℤ ℂ)).rootMultiplicity x)
    (hunique : ∀ y : ℂ, 1 < (g.val.charpoly.map (algebraMap ℤ ℂ)).rootMultiplicity y → y = x) :
    x = 1 ∨ x = -1 := by
…