mem_cycles₁_iff — Mathlib

English

A pure basis element single g a lies in Z1(G,A) exactly when ρ_A(g) a = a.

Русский

Чистый элемент-генератор single g a принадлежит Z1(G,A) тогда и только тогда, когда ρ_A(g) a = a.

LaTeX

$$single g a ∈ Z_1(G,A) \iff A.ρ g a = a$$

Lean4

theorem mem_cycles₁_iff (x : G →₀ A) : x ∈ cycles₁ A ↔ x.sum (fun g a => A.ρ g⁻¹ a) = x.sum (fun _ a => a) :=
  by
  change x.sum (fun g a => A.ρ g⁻¹ a - a) = 0 ↔ _
  rw [sum_sub, sub_eq_zero]

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