smithCoeffs_ne_zero — Mathlib

English

Each Smith coefficient corresponding to the embedding of I into S is nonzero.

Русский

Каждый коэффициент Смита, соответствующий включению I в S, не равен нулю.

LaTeX

$$$\\forall i,\\; \\text{smithCoeffs } b I hI i \\neq 0$$$

Lean4

@[simp]
theorem smithCoeffs_ne_zero (b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) (i) : Ideal.smithCoeffs b I hI i ≠ 0 :=
  by
  intro hi
  apply Basis.ne_zero (Ideal.selfBasis b I hI) i
  refine Subtype.coe_injective ?_
  simp [hi]

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