basisOfIsMaxRank — Mathlib

English

Given a maximal rank family u, the images under logEmbedding form a basis of logSpace K.

Русский

Для семейства единиц максимального ранга изображения через logEmbedding образуют базис в пространстве logSpace K.

LaTeX

$$$\\text{basisOfIsMaxRank}(u, hu) : \\text{Basis}(\\mathrm{Fin}(\\mathrm{rank}\\,K))\\;\\mathbb{R}\\;\\mathrm{logSpace}(K).$$$

Lean4

/-- The images by `logEmbedding` of a family of units of maximal rank form a basis of `logSpace K`.
-/
def basisOfIsMaxRank {u : Fin (rank K) → (𝓞 K)ˣ} (hu : IsMaxRank u) : Basis (Fin (rank K)) ℝ (logSpace K) :=
  (basisOfPiSpaceOfLinearIndependent ((linearIndependent_equiv (equivFinRank K).symm).mpr hu)).reindex
    (equivFinRank K).symm

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