toSubmodule_range — Mathlib

English

For a LieModuleHom f: M →ₗ⁅R,L⁆ N, the range considered as a Lie submodule of N equals the range of the underlying linear map: f.range = LinearMap.range (f : M →ₗ[R] N).

Русский

Для гомоморфа Ли-модулей f: M →ₗ⁅R,L⁆ N образ, рассматриваемый как подмодуль N, равен образу линейного отображения: f.range = LinearMap.range (f : M →ₗ[R] N).

LaTeX

$$$f.range = \operatorname{LinearMap.range}(f : M \to[R] N)$$$

Lean4

@[simp]
theorem toSubmodule_range : f.range = LinearMap.range (f : M →ₗ[R] N) :=
  rfl

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