LeanPool.LeanPolyABC.Corollaries.NoParametrization

def LeanPolyABC.IsConst {k : Type u_1} [Field k] (x : RatFunc k) : Prop

A rational function is constant if it equals RatFunc.C c for some scalar c.

Equations

• LeanPolyABC.IsConst x = ∃ (c : k), x = RatFunc.C c

theorem LeanPolyABC.associates_pow_eq_pow_iff {k : Type u_1} [Field k] {A B : Associates (Polynomial k)} {n : ℕ} (hn : n ≠ 0) : A ^ n = B ^ n ↔ A = B

theorem LeanPolyABC.isConst_of_associated {k : Type u_1} [Field k] {f : RatFunc k} (h : Associated f.num f.denom) : IsConst f

theorem LeanPolyABC.isConst_of_root_unity {k : Type u_1} [Field k] {n : ℕ} (hn : n ≠ 0) {f : RatFunc k} (h : f ^ n = 1) : IsConst f

theorem LeanPolyABC.associated_pow_pow_coprime_iff {k : Type u_1} [Field k] {a b : Polynomial k} {m n : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (_hm : m ≠ 0) (hn : n ≠ 0) (h : Associated (a ^ m) (b ^ n)) (hcp : m.Coprime n) : ∃ (c : Polynomial k), c ≠ 0 ∧ Associated a (c ^ n) ∧ Associated b (c ^ m)

theorem LeanPolyABC.calcstep {k : Type u_1} [Field k] {n N m M : Polynomial k} (nz_M : M ≠ 0) (nz_N : N ≠ 0) (eqn : (algebraMap (Polynomial k) (RatFunc k)) n ^ 2 / (algebraMap (Polynomial k) (RatFunc k)) N ^ 2 = (algebraMap (Polynomial k) (RatFunc k)) m ^ 3 / (algebraMap (Polynomial k) (RatFunc k)) M ^ 3 + 1) : n ^ 2 * M ^ 3 = (m ^ 3 + M ^ 3) * N ^ 2

theorem LeanPolyABC.calcstep2 {k : Type u_1} [Field k] {m M n N : Polynomial k} (nz_M : M ≠ 0) (nz_N : N ≠ 0) (cp_mM : IsCoprime m M) (cp_nN : IsCoprime n N) (_nz_m : m ≠ 0) (_nz_n : n ≠ 0) (flat_eqn : n ^ 2 * M ^ 3 = (m ^ 3 + M ^ 3) * N ^ 2) : ∃ (w : Polynomial k) (u : (Polynomial k)ˣ) (v : (Polynomial k)ˣ), w ≠ 0 ∧ ↑u * w ^ 2 = M ∧ ↑v * w ^ 3 = N ∧ IsCoprime m w ∧ ↑u ^ 3 * n ^ 2 = ↑v ^ 2 * m ^ 3 + ↑v ^ 2 * ↑u ^ 3 * w ^ 6

theorem LeanPolyABC.no_parametrization_y2_x3_1 {k : Type u_1} [Field k] (chk : ¬ringChar k ∣ 6) {x y : RatFunc k} (eqn : y ^ 2 = x ^ 3 + 1) : IsConst x ∧ IsConst y