ker_toSubmodule

Mathlib.Algebra.Lie.Ideal

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

English

The comap operation is monotone with respect to inclusion of LieIdeals.

Русский

Операция обратного образа монотонна по включениям Ли-идеалов.

LaTeX

$$Monotone (comap f)$$

Lean4

@[simp]
theorem ker_toSubmodule : LieSubmodule.toSubmodule (ker f) = LinearMap.ker (f : L →ₗ[R] L') :=
  rfl

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

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

Разделы

Аффилиация

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