mk_bracket

Mathlib.Algebra.Lie.Quotient

URI: https://scilib.ai/kg/mathlib#LieSubmodule.Quotient.mk_bracket

Lean4

@[simp]
theorem mk_bracket (x y : L) : mk ⁅x, y⁆ = ⁅(mk x : L ⧸ I), (mk y : L ⧸ I)⁆ :=
  rfl

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

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

Разделы

Аффилиация

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