d₁₀_eq_zero_of_isTrivial

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

URI: https://scilib.ai/kg/mathlib#groupHomology.d₁₀_eq_zero_of_isTrivial

English

If A is the trivial G-representation, then the differential d10 is identically zero.

Русский

Если A — тривиальное представление группы G, то дифференциал d10 тождественно равен нулю.

LaTeX

$$$[A\text{ isTrivial}] \Rightarrow d_{10}A = 0$$$

Lean4

@[simp]
theorem d₁₀_eq_zero_of_isTrivial [A.IsTrivial] : d₁₀ A = 0 :=
  by
  ext
  simp [d₁₀]

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

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

Разделы

Аффилиация

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