cycles₁IsoOfIsTrivial_inv_apply

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

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

English

The inverse part of the isomorphism reverses x to itself when viewed in the underlying component.

Русский

Обратная часть изоморфизма возвращает x к самому себе в базовом компоненте.

LaTeX

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

Lean4

@[simp]
theorem cycles₁IsoOfIsTrivial_inv_apply [A.IsTrivial] (x : G →₀ A) : ((cycles₁IsoOfIsTrivial A).inv x).1 = x :=
  rfl

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

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

Разделы

Аффилиация

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