coord — Mathlib

English

The span coordinate map coord is defined as the inverse of the span isomorphism, giving a canonical isomorphism coord: (R·x) ≃ₗ[R] R.

Русский

Координатная изomорфия coord задаётся как обратная к изоморфизму span; получается канонический линейный эквивалент coord: (R·x) ≃ₗ[R] R.

LaTeX

$$$ coord = (toSpanNonzeroSingleton R M x h)^{-1} : (R \cdot x) \cong_R R. $$$

Lean4

/-- Given a nonzero element `x` of a torsion-free module `M` over a ring `R`, the natural
isomorphism from the span of `x` to `R` given by $r \cdot x \mapsto r$. -/
noncomputable abbrev coord : (R ∙ x) ≃ₗ[R] R :=
  (toSpanNonzeroSingleton R M x h).symm

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