coe_lift_symm

Mathlib.GroupTheory.Abelianization.Defs

URI: https://scilib.ai/kg/mathlib#Abelianization.coe_lift_symm

English

The inverse of lift corresponds to composing with of: (lift.symm) f = f ∘ of.

Русский

Обратный к lift частично задаётся как композиция с of: lift.symm f = f ∘ of.

LaTeX

$$$$ \\mathrm{lift}.symm(f) = f \\circ \\mathrm{of}. $$$$

Lean4

theorem coe_lift_symm : (lift.symm : (Abelianization G →* A) → (G →* A)) = (·.comp of) :=
  rfl

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

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

Разделы

Аффилиация

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