toSpanNonzeroSingleton_one — Mathlib

English

The image of 1 under the span isomorphism t ↦ t·x is the generator element of the span, i.e., it is the vector x itself inside R·x.

Русский

Образ единицы под изоморфизмом R → R·x равен порождающему элементу: единица отображается в x внутри R·x.

LaTeX

$$$ (toSpanNonzeroSingleton R M x h)(1) = \langle x, \operatorname{Submodule.mem\_span\_singleton\_self} x \rangle. $$$

Lean4

theorem toSpanNonzeroSingleton_one :
    LinearEquiv.toSpanNonzeroSingleton R M x h 1 = (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x) := by simp

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