lift_of'

Mathlib.GroupTheory.CoprodI

URI: https://scilib.ai/kg/mathlib#Monoid.CoprodI.lift_of'

English

The lift with the injections of every summand equals the identity map on CoprodI(M).

Русский

Lift, взятый по всем инъекциям (of_i), равен тождественному отображению на CoprodI(M).

LaTeX

$$$\\mathrm{lift}(\\,i \\mapsto \\mathrm{of}) = \\mathrm{id}_{\\mathrm{CoprodI}(M)}$$$

Lean4

@[simp]
theorem lift_of' : lift (fun i ↦ (of : M i →* CoprodI M)) = .id (CoprodI M) :=
  lift_comp_of' (.id _)

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

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

Разделы

Аффилиация

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