mem_cycles₂_iff — Mathlib

English

For x ∈ G × G →₀ A, x ∈ Z2(G,A) iff the equality ∑ g a equals ∑ (g1 g2) a holds with the two summands given by d21’s target, i.e. the boundary condition.

Русский

Для x ∈ G×G →₀ A верно: x ∈ Z2(G,A) тогда, когда сумма по парам (g1,g2) соответствует границе d21.

LaTeX

$$x ∈ Z_2(G,A) ⇔ x.sum (fun g a => single g.2 (A.ρ g.1⁻¹ a) + single g.1 a) = x.sum (fun g a => single (g.1 * g.2) a)$$

Lean4

theorem mem_cycles₂_iff (x : G × G →₀ A) :
    x ∈ cycles₂ A ↔
      x.sum (fun g a => single g.2 (A.ρ g.1⁻¹ a) + single g.1 a) = x.sum (fun g a => single (g.1 * g.2) a) :=
  by
  change x.sum (fun g a => _) = 0 ↔ _
  simp [sub_add_eq_add_sub, sub_eq_zero]

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