H0IsoOfIsTrivial_inv_apply

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupCohomology.H0IsoOfIsTrivial_inv_apply

English

The inverse of H0IsoOfIsTrivial sends x ∈ A.V to its canonical representative in H0.

Русский

Обратное отображение H0IsoOfIsTrivial отправляет x ∈ A.V в канонический представитель в H0.

LaTeX

$$(H0IsoOfIsTrivial A).inv x = (H0Iso A).inv ⟨x, by simp⟩$$

Lean4

@[simp]
theorem H0IsoOfIsTrivial_inv_apply (x : A) : (H0IsoOfIsTrivial A).inv x = (H0Iso A).inv ⟨x, by simp⟩ :=
  rfl

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

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

Разделы

Аффилиация

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