basisOfIsMaxRank_apply — Mathlib

English

A key equality: the function-valued basis defined via basisOfIsMaxRank coincides with the reindexed basis coming from logEmbedding, under an isomorphism.

Русский

Ключевое равенство: базис, заданный через basisOfIsMaxRank, совпадает с перераспределённым базисом, полученным из logEmbedding, через изоморфизм.

LaTeX

$$$\\text{basisOfIsMaxRank\_eq\_1}(hu) : \\,(\\text{basisOfIsMaxRank}\,hu) = (\\text{basisOfPiSpaceOfLinearIndependent}\\,\\dots).$$$

Lean4

@[simp]
theorem basisOfIsMaxRank_apply {u : Fin (rank K) → (𝓞 K)ˣ} (hu : IsMaxRank u) (i : Fin (rank K)) :
    (basisOfIsMaxRank hu) i = logEmbedding K (Additive.ofMul (u i)) := by
  simp [basisOfIsMaxRank, Basis.coe_reindex, Equiv.symm_symm, Function.comp_apply,
    coe_basisOfPiSpaceOfLinearIndependent]

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