map_sup_ker_eq_map'

Mathlib.Algebra.Lie.Ideal

URI: https://scilib.ai/kg/mathlib#LieIdeal.map_sup_ker_eq_map'

← MathLib Explorer

English

A simplified version: LieIdeal.map f I ⊔ LieIdeal.map f (ker f) = LieIdeal.map f I.

Русский

Упрощенная формула: I.map f ⊔ I.map f (ker f) = I.map f.

LaTeX

$$$\operatorname{map} f\ I \;\sqcup\; \operatorname{map} f(\ker f) = \operatorname{map} f I$$$

Lean4

@[simp]
theorem map_sup_ker_eq_map' : LieIdeal.map f I ⊔ LieIdeal.map f (LieHom.ker f) = LieIdeal.map f I := by
  simpa using map_sup_ker_eq_map (f := f)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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