smithNormalFormCoeffs_ne_zero — Mathlib

English

The Smith normal form coefficients are nonzero for each index i in ι.

Русский

Коэффициенты Смитт-формы не нулевые для каждого индекса i.

LaTeX

$$$\\forall i,\\; smithNormalFormCoeffs b h i \\neq 0$$$

Lean4

@[simp]
theorem smithNormalFormCoeffs_ne_zero (b : Basis ι R M) (h : Module.finrank R N = Module.finrank R M) (i : ι) :
    smithNormalFormCoeffs b h i ≠ 0 := by
  intro hi
  apply Basis.ne_zero (smithNormalFormBotBasis b h) i
  refine Subtype.coe_injective ?_
  simp [hi]

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