range_toSubmodule

Mathlib.Algebra.Lie.Ideal

URI: https://scilib.ai/kg/mathlib#LieHom.range_toSubmodule

English

The range of f, as a submodule, equals the Submodule range of the linear map underlying f.

Русский

Образ f как подмодуль равен Submodule range линейного отображения, лежащего в основе f.

LaTeX

$$$\\text{range}(f) = \\text{range}(f)_{toSubmodule}$$$

Lean4

@[simp]
theorem range_toSubmodule : (f.range : Submodule R L') = LinearMap.range (f : L →ₗ[R] L') :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru