class_eq

Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous.class_eq

English

If IsCohomologous holds, then γ1.class = γ2.class.

Русский

Если IsCohomologous выполняется, то γ1.class = γ2.class.

LaTeX

$$γ₁.class = γ₂.class$$

Lean4

theorem class_eq {γ₁ γ₂ : OneCocycle G U} (h : γ₁.IsCohomologous γ₂) : γ₁.class = γ₂.class :=
  Quot.sound h

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

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

Разделы

Аффилиация

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