one — Mathlib

English

The unit (1) in Submodule R A is defined as the range of the span singleton map sending 1 to A.

Русский

Единица (1) в Submodule R A определяется как образ отображения span-singleton, отправляющего 1 в A.

LaTeX

$$$(1 : Submodule\\, R\\, A) = \\mathrm{range}(\\mathrm{toSpanSingleton}\\, R\\, A\\, 1)$$$

Lean4

/-- `1 : Submodule R A` is the submodule `R ∙ 1` of `A`.
-/
instance one : One (Submodule R A) :=
  ⟨LinearMap.range (LinearMap.toSpanSingleton R A 1)⟩

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