d₁₀_single

Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

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

English

For g in G and a in A, d1_0(single g^{-1} a) = - d1_0(single g ρ(g) a).

Русский

Для элемента g и a ∈ A выполняется d1_0(single g^{-1} a) = - d1_0(single g ρ(g) a).

LaTeX

$$$d_{10} A (single g^{-1} a) = -d_{10} A (single g (A.\rho g a))$$$

Lean4

@[simp]
theorem d₁₀_single (g : G) (a : A) : d₁₀ A (single g a) = A.ρ g⁻¹ a - a := by simp [d₁₀]

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

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

Разделы

Аффилиация

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