instZero

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieModuleHom.instZero

English

There exists a zero Lie module morphism from M to N.

Русский

Существет нулевой морфизм Ли-модуля из M в N.

LaTeX

$$$0 : M →ₗ⁅R,L⁆ N$ exists and is a Lie module homomorphism.$$

Lean4

/-- The constant 0 map is a Lie module morphism. -/
instance : Zero (M →ₗ⁅R,L⁆ N) :=
  ⟨{ (0 : M →ₗ[R] N) with map_lie' := by simp }⟩

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

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

Разделы

Аффилиация

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