cycles₁_eq_top_of_isTrivial — Mathlib

English

There is a natural isomorphism between Z1(G,A) and G →₀ A when A is a trivial representation.

Русский

Существует естественный изоморфизм между Z1(G,A) и G →₀ A, если A тривиально как представление.

LaTeX

$$Z_1(G,A) \cong G \to_0 A \quad\text{when } A \text{ is trivial}$$

Lean4

theorem cycles₁_eq_top_of_isTrivial [A.IsTrivial] : cycles₁ A = ⊤ := by
  rw [cycles₁, d₁₀_eq_zero_of_isTrivial, ModuleCat.hom_zero, LinearMap.ker_zero]

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