LeanPool.LeanPolyABC.MasonStothers

theorem LeanPolyABC.Ne.isUnit_C {k : Type u_1} [Field k] {u : k} (hu : u ≠ 0) : IsUnit (Polynomial.C u)

theorem LeanPolyABC.Ne.C_ne_zero {k : Type u_1} [Field k] {u : k} (hu : u ≠ 0) : Polynomial.C u ≠ 0

theorem LeanPolyABC.dvd_derivative_iff {k : Type u_1} [Field k] {a : Polynomial k} : a ∣ Polynomial.derivative a ↔ Polynomial.derivative a = 0

theorem LeanPolyABC.IsCoprime.wronskian_eq_zero_iff {k : Type u_1} [Field k] {a b : Polynomial k} (hc : IsCoprime a b) : wronskian a b = 0 ↔ Polynomial.derivative a = 0 ∧ Polynomial.derivative b = 0

theorem LeanPolyABC.IsCoprime.divRadical {k : Type u_1} [Field k] [DecidableEq k] {a b : Polynomial k} (h : IsCoprime a b) : IsCoprime (Polynomial.divRadical a) (Polynomial.divRadical b)

theorem LeanPolyABC.Polynomial.abc {k : Type u_1} [Field k] [DecidableEq k] {a b c : Polynomial k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (hsum : a + b + c = 0) : Polynomial.derivative a = 0 ∧ Polynomial.derivative b = 0 ∧ Polynomial.derivative c = 0 ∨ a.natDegree.max₃ b.natDegree c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

theorem LeanPolyABC.Polynomial.abc_char0 {k : Type u_1} [Field k] [DecidableEq k] [CharZero k] {a b c : Polynomial k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (hsum : a + b + c = 0) : a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0 ∨ a.natDegree.max₃ b.natDegree c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

theorem LeanPolyABC.isUnit_iff_natDegree_eq_zero {k : Type u_1} [Field k] {a : Polynomial k} (ha : a ≠ 0) : IsUnit a ↔ a.natDegree = 0

theorem LeanPolyABC.natDegree_radical_eq_zero_iff {k : Type u_1} [Field k] [DecidableEq k] {a : Polynomial k} : (radical a).natDegree = 0 ↔ a.natDegree = 0

theorem LeanPolyABC.Polynomial.abc'_char0 {k : Type u_1} [Field k] [DecidableEq k] [CharZero k] {a b c : Polynomial k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hsum : a + b + c = 0) : a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0 ∨ a.natDegree.max₃ b.natDegree c.natDegree + 1 ≤ (radical a).natDegree + (radical b).natDegree + c.natDegree