ofCoprodI

Mathlib.GroupTheory.PushoutI

URI: https://scilib.ai/kg/mathlib#Monoid.PushoutI.ofCoprodI

English

Equality relating ofCoprodI and PushoutI.mor on generators: ofCoprodI (CoprodI.of g) = of i g

Русский

Сопоставление ofCoprodI и of_i на генераторах: ofCoprodI (CoprodI.of g) = of_i g

LaTeX

$$ofCoprodI (CoprodI.of g) = of_i g$$

Lean4

/-- The map from the coproduct into the pushout -/
def ofCoprodI : CoprodI G →* PushoutI φ :=
  CoprodI.lift of

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

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

Разделы

Аффилиация

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