isCocycle₂_of_mem_cocycles₂ — Mathlib

English

If f ∈ cocycles2 (Rep.ofDistribMulAction k G A), then IsCocycle2 f.

Русский

Если f ∈ cocycles2 (Rep.ofDistribMulAction k G A), тогда IsCocycle2 f.

LaTeX

$$$f \in \text{cocycles}_2(\mathrm{Rep.ofDistribMulAction}\; k\; G\; A) \Rightarrow \text{IsCocycle}_2 f$$$

Lean4

theorem isCocycle₂_of_mem_cocycles₂ (f : G × G → A) (hf : f ∈ cocycles₂ (Rep.ofDistribMulAction k G A)) :
    IsCocycle₂ f :=
  (mem_cocycles₂_iff (A := Rep.ofDistribMulAction k G A) f).1 hf

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