repr_eq_zero_of_notMem_range — Mathlib

English

If a submodule N has the same rank as M, there exists Smith normal form data with equal rank components linking the bases of N and M.

Русский

Если ранг подмодуля N равен рангу M, существует форма SmithNormalForm со связующими данными между базами N и M.

LaTeX

$$$\\exists o, n, hno, bO, bN, a \\;\\text{such that }\\forall i, (bN i) = a i · (bO (Fin.castLE hno i))$$$

Lean4

theorem repr_eq_zero_of_notMem_range {i : ι} (hi : i ∉ Set.range snf.f) : snf.bM.repr m i = 0 :=
  by
  obtain ⟨m, hm⟩ := m
  obtain ⟨c, rfl⟩ := snf.bN.mem_submodule_iff.mp hm
  replace hi : ∀ j, snf.f j ≠ i := by simpa using hi
  simp [hi, snf.snf, map_finsuppSum]

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