ker_eq_bot

Mathlib.Algebra.Lie.Abelian

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

English

If the action is faithful, then the kernel is the zero submodule.

Русский

Если действие исчерпывающее (faithful), то ядро равно нулевому подмодулю.

LaTeX

$$$\\mathrm{ker}(R,L,M) = \\{0\\}$ when the action is faithful.$$

Lean4

@[simp]
theorem ker_eq_bot [IsFaithful R L M] : LieModule.ker R L M = ⊥ :=
  (isFaithful_iff_ker_eq_bot R L M).mp inferInstance

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

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

Разделы

Аффилиация

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