Discr_ne_zero_of_normalForm_split.lean

theorem coeff_prod_of_natDegree_le {R : Type*} [CommRing R] {ι : Type*} (s : Finset ι)
    (f : ι → R[X]) (N : ι → ℕ) (h : ∀ i ∈ s, (f i).natDegree ≤ N i) :
    (∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, N i ∧
      (∏ i ∈ s, f i).coeff (∑ i ∈ s, N i) = ∏ i ∈ s, (f i).coeff (N i)

theorem main (b : Module.Basis (Fin (n + 1)) K[X] B) (d : Fin (n + 1) → ℕ)
    (hb0 : b 0 = 1) (hd0 : d 0 = 0) (hd : ∀ i, i ≠ 0 → d i = 1 ∨ d i = 2)
    (hdeg : ∀ i j k, i ≠ 0 → j ≠ 0 → ((b.repr (b i * b j)) k).natDegree ≤ d i + d j - d k)
    (τ : Fin (n + 1) → Fin (n + 1) → K) (hτu : IsUnit (Matrix.det (Matrix.of τ)))
    (hτ0 : ∀ j, τ j 0 = 1)
    (hτm : ∀ j i i', i ≠ 0 → i' ≠ 0 →
      τ j i * τ j i' = ∑ k, ((b.repr (b i * b i')) k).coeff (d i + d i' - d k) * τ j k) :
    Algebra.discr K[X] b ≠ 0

theorem _root_.AlgebraicCurve.discr_ne_zero_of_normalForm_split
    (K : Type u) [Field K] (n : ℕ) (B : Type v) [CommRing B] [Algebra K[X] B]
    (b : Module.Basis (Fin (n + 1)) K[X] B) (d : Fin (n + 1) → ℕ)
    (hb0 : b 0 = 1) (hd0 : d 0 = 0) (hd : ∀ i, i ≠ 0 → d i = 1 ∨ d i = 2)
    (hdeg : ∀ i j k, i ≠ 0 → j ≠ 0 → ((b.repr (b i * b j)) k).natDegree ≤ d i + d j - d k)
    (hinf : ∃ τ : Fin (n + 1) → Fin (n + 1) → K,
      IsUnit (Matrix.det (Matrix.of τ)) ∧
      (∀ j, τ j 0 = 1) ∧
      ∀ j i i', i ≠ 0 → i' ≠ 0 →
        τ j i * τ j i' = ∑ k, ((b.repr (b i * b i')) k).coeff (d i + d i' - d k) * τ j k) :
    Algebra.discr K[X] b ≠ 0