smithNormalFormBotBasis_def — Mathlib

English

For each i, the i-th vector in smithNormalFormBotBasis is the product of smithNormalFormCoeffs and smithNormalFormTopBasis at i.

Русский

Для каждого i вектор i-й позиции smithNormalFormBotBasis равен произведению coeff_i и i-й вершины smithNormalFormTopBasis.

LaTeX

$$$\\forall i,\\; (smithNormalFormBotBasis b h i) = smithNormalFormCoeffs b h i \\cdot smithNormalFormTopBasis b h i$$$

Lean4

@[simp]
theorem smithNormalFormBotBasis_def (b : Basis ι R M) (h : Module.finrank R N = Module.finrank R M) :
    ∀ i, (smithNormalFormBotBasis b h i : M) = smithNormalFormCoeffs b h i • smithNormalFormTopBasis b h i :=
  (exists_smith_normal_form_of_rank_eq b h).choose_spec.choose_spec.choose_spec

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