is_quotient_mk

Mathlib.Algebra.Lie.Quotient

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

English

The quotient construction is compatible with mk, i.e., mk'' m equals mk m in M/N.

Русский

Конструкция фактор-пространства совместима с mk; mk'' m равно mk m в M/N.

LaTeX

$$Quotient.mk'' m = (mk m)$$

Lean4

theorem is_quotient_mk (m : M) : Quotient.mk'' m = (mk m : M ⧸ N) :=
  rfl

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

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

Разделы

Аффилиация

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