isCoboundary₁_of_mem_coboundaries₁

English

If f ∈ coboundaries1 (Rep.ofDistribMulAction k G A), then IsCoboundary1 f.

Русский

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

LaTeX

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

Lean4

theorem isCoboundary₁_of_mem_coboundaries₁ (f : G → A) (hf : f ∈ coboundaries₁ (Rep.ofDistribMulAction k G A)) :
    IsCoboundary₁ f := by
  rcases hf with ⟨a, rfl⟩
  exact ⟨a, fun _ => rfl⟩

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