val_eq_coe

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupCohomology.cocycles₁.val_eq_coe

English

The underlying function of the cocycle constructor equals the given function f.

Русский

Для конструкторa кокицелей 1–циклa функция-основание совпадает с данным f.

LaTeX

$$coe_mk (f : G → A) (hf) : ((⟨f, hf⟩ : cocycles_1 A) : G → A) = f$$

Lean4

@[simp]
theorem val_eq_coe (f : cocycles₁ A) : f.1 = f :=
  rfl

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

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

Разделы

Аффилиация

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