mulRight_one

Mathlib.CategoryTheory.Monoidal.Grp_

URI: https://scilib.ai/kg/mathlib#GrpObj.mulRight_one

English

The right multiplication by the unit is the identity isomorphism: mulRight(η_A) = Iso.refl A.

Русский

Правая умножение на единицу эквивалентно тождественному изоморфизму: mulRight(η_A) = Iso.refl A.

LaTeX

$$$\mathrm{mulRight}(\eta_A) = \mathrm{Iso.refl}(A)$$$

Lean4

@[simp]
theorem mulRight_one (A : C) [GrpObj A] : mulRight η[A] = Iso.refl A := by ext; simp

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

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

Разделы

Аффилиация

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