repr — Mathlib

English

There is a canonical linear isomorphism between M and the free module on its basis index.

Русский

Существует каноническое линейное изоморфизм между M и свободной модулем на его индексном базисе.

LaTeX

$$$$ M \cong_R (\mathrm{ChooseBasisIndex}(R,M) \to_0 R) $$$$

Lean4

/-- The isomorphism `M ≃ₗ[R] (ChooseBasisIndex R M →₀ R)`. -/
@[deprecated Module.Free.chooseBasis (since := "2025-08-01")]
noncomputable def repr : M ≃ₗ[R] ChooseBasisIndex R M →₀ R :=
  (chooseBasis R M).repr

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