LeanPool.LeanPolyABC.Corollaries.FltCatalan

theorem LeanPolyABC.weighted_average_le_max₃ {p q r a b c : ℕ} : p * a + q * b + r * c ≤ (p + q + r) * a.max₃ b c

theorem LeanPolyABC.derivative_pow_eq_zero_iff {k : Type u_1} [Field k] {n : ℕ} (chn : ¬ringChar k ∣ n) {a : Polynomial k} : Polynomial.derivative (a ^ n) = 0 ↔ Polynomial.derivative a = 0

theorem LeanPolyABC.mul_eq_zero_left_iff {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} (ha : a ≠ 0) : a * b = 0 ↔ b = 0

theorem LeanPolyABC.Polynomial.flt_catalan_deriv {k : Type u_1} [Field k] {p q r : ℕ} (hp : 0 < p) (hq : 0 < q) (hr : 0 < r) (hineq : q * r + r * p + p * q ≤ p * q * r) (chp : ¬ringChar k ∣ p) (chq : ¬ringChar k ∣ q) (chr : ¬ringChar k ∣ r) {a b c : Polynomial k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) {u v w : k} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) (heq : Polynomial.C u * a ^ p + Polynomial.C v * b ^ q + Polynomial.C w * c ^ r = 0) : Polynomial.derivative a = 0 ∧ Polynomial.derivative b = 0 ∧ Polynomial.derivative c = 0

theorem LeanPolyABC.Polynomial.flt_catalan_aux {k : Type u_1} [Field k] {p q r : ℕ} (hp : 0 < p) (hq : 0 < q) (hr : 0 < r) (hineq : q * r + r * p + p * q ≤ p * q * r) (chp : ¬ringChar k ∣ p) (chq : ¬ringChar k ∣ q) (chr : ¬ringChar k ∣ r) {a b c : Polynomial k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) {u v w : k} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) (heq : Polynomial.C u * a ^ p + Polynomial.C v * b ^ q + Polynomial.C w * c ^ r = 0) : a.natDegree = 0

theorem LeanPolyABC.Polynomial.flt_catalan {k : Type u_1} [Field k] {p q r : ℕ} (hp : 0 < p) (hq : 0 < q) (hr : 0 < r) (hineq : q * r + r * p + p * q ≤ p * q * r) (chp : ¬ringChar k ∣ p) (chq : ¬ringChar k ∣ q) (chr : ¬ringChar k ∣ r) {a b c : Polynomial k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) {u v w : k} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) (heq : Polynomial.C u * a ^ p + Polynomial.C v * b ^ q + Polynomial.C w * c ^ r = 0) : a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

theorem LeanPolyABC.Polynomial.flt {k : Type u_1} [Field k] {n : ℕ} (hn : 3 ≤ n) (chn : ¬ringChar k ∣ n) {a b c : Polynomial k} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (heq : a ^ n + b ^ n = c ^ n) : a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0