smul_basis_eq_zero — Mathlib

English

If a linear combination p•1 + q•mk W' Y is equal to zero, then p and q must be zero polynomials in R[X].

Русский

Если линейная комбинация p•1 + q•mk W' Y равна нулю, значит p и q должны быть нулями полиномами.

LaTeX

$$p • 1 + q • mk W' Y = 0 \Rightarrow p = 0 ∧ q = 0$$

Lean4

theorem smul_basis_eq_zero {p q : R[X]} (hpq : p • (1 : W'.CoordinateRing) + q • mk W' Y = 0) : p = 0 ∧ q = 0 :=
  by
  have h := Fintype.linearIndependent_iff.mp (CoordinateRing.basis W').linearIndependent ![p, q]
  rw [Fin.sum_univ_succ, basis_zero, Fin.sum_univ_one, Fin.succ_zero_eq_one, basis_one] at h
  exact ⟨h hpq 0, h hpq 1⟩

Похожие утверждения