cycles₁IsoOfIsTrivial_hom_apply

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupHomology.cycles₁IsoOfIsTrivial_hom_apply

English

For any x in the domain of Z1, the hom part of the isomorphism sends x to itself.

Русский

Для любого x из Z1 отображение гомоморфной части изоморфизма отправляет x в само x.

LaTeX

$$(cycles₁IsoOfIsTrivial A).hom x = x$$

Lean4

@[simp]
theorem cycles₁IsoOfIsTrivial_hom_apply [A.IsTrivial] (x : cycles₁ A) : (cycles₁IsoOfIsTrivial A).hom x = x.1 :=
  rfl

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

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

Разделы

Аффилиация

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