extendOfIsLattice_apply — Mathlib

English

If b is a basis of an R-lattice M, then evaluating its extension on an index k gives the corresponding vector from M, i.e., b.extendOfIsLattice K k = (b k).val.

Русский

Если b — базис R-решётки M, то применение расширения к индексу k возвращает соответствующий вектор из M: b.extendOfIsLattice K k = (b k).val.

LaTeX

$$$b.extendOfIsLattice(K)\,k = (b\,k).\text{val}$$$

Lean4

@[simp]
theorem _root_.Module.Basis.extendOfIsLattice_apply [IsFractionRing R K] {κ : Type*} {M : Submodule R V} [IsLattice K M]
    (b : Basis κ R M) (k : κ) : b.extendOfIsLattice K k = (b k).val := by simp [Basis.extendOfIsLattice]

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