lift_inr_inl

Mathlib.GroupTheory.Coprod.Basic

URI: https://scilib.ai/kg/mathlib#Monoid.Coprod.lift_inr_inl

English

There is a canonical equality of monoid homomorphisms: lift (inr, inl) equals swap.

Русский

Существует каноническое равенство гомоморфизмов: lift (inr, inl) равен swap.

LaTeX

$$$ \operatorname{lift}(\mathrm{inr}, \mathrm{inl}) = \mathrm{swap}. $$$

Lean4

@[to_additive (attr := simp)]
theorem lift_inr_inl : lift (inr : M →* N ∗ M) inl = swap M N :=
  hom_ext rfl rfl

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

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

Разделы

Аффилиация

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