toEnd_eq_zero_iff

Mathlib.Algebra.Lie.OfAssociative

URI: https://scilib.ai/kg/mathlib#LieModule.toEnd_eq_zero_iff

English

For a faithful LieModule, the endomorphism corresponding to x is zero if and only if x is zero.

Русский

При истинности Faithful: toEnd x = 0 ⇔ x = 0.

LaTeX

$$$$ toEnd_R L M \; x = 0 \;\iff\; x = 0.$$$$

Lean4

@[simp]
theorem toEnd_eq_zero_iff [IsFaithful R L M] {x : L} : toEnd R L M x = 0 ↔ x = 0 := by
  simp [-LieHom.map_zero, ← (toEnd R L M).map_zero]

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

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

Разделы

Аффилиация

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