isCocycle₁_of_mem_cocycles₁ — Mathlib

English

If f ∈ cocycles1 (Rep.ofDistribMulAction k G A), then IsCocycle1 f.

Русский

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

LaTeX

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

Lean4

theorem isCocycle₁_of_mem_cocycles₁ (f : G → A) (hf : f ∈ cocycles₁ (Rep.ofDistribMulAction k G A)) : IsCocycle₁ f :=
  fun _ _ => (mem_cocycles₁_iff (A := Rep.ofDistribMulAction k G A) f).1 hf _ _

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