one_eq_range — Mathlib

English

The unit submodule (1) equals the range of the algebra linear map: (1 : Submodule R A) = LinearMap.range (Algebra.linearMap R A).

Русский

Единичный подпмодуль равняется образу линейного отображения алгебры: (1) = Range(Algebra.linearMap R A).

LaTeX

$$$ (1 : Submodule R A) = LinearMap.range (Algebra.linearMap R A) $$$

Lean4

theorem one_eq_range : (1 : Submodule R A) = LinearMap.range (Algebra.linearMap R A) := by
  rw [one_eq_span, LinearMap.span_singleton_eq_range, LinearMap.toSpanSingleton_eq_algebra_linearMap]

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