prod_fst_snd

Mathlib.GroupTheory.GroupAction.Hom

URI: https://scilib.ai/kg/mathlib#MulActionHom.prod_fst_snd

English

The product of the projection maps equals the identity map on the acting structure.

Русский

Произведение проекций равно единичному отображению на структуре действия.

LaTeX

$$$prod\; (fst\ M\ α\ β)\ (snd\ M\ α\ β) = .id\ ..$$$

Lean4

@[to_additive (attr := simp) prod_fst_snd]
theorem prod_fst_snd : prod (fst M α β) (snd M α β) = .id .. :=
  rfl

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

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

Разделы

Аффилиация

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