isIso_δ_of_isZero — Mathlib

English

If H^n(G,X2) and H^{n+1}(G,X2) vanish, then δ is an isomorphism.

Русский

Если нулевые когомологии на местах X2 на n и n+1 равны, δ является изоморфизмом.

LaTeX

$$$\text{isIso}_δ(n,hX, h, hs): δ: H^n(G,X_3) \to H^{n+1}(G,X_1) \text{ isomorphism}$$$

Lean4

theorem isIso_δ_of_isZero (n : ℕ) (h : IsZero (groupCohomology X.X₂ n)) (hs : IsZero (groupCohomology X.X₂ (n + 1))) :
    IsIso (δ hX n (n + 1) rfl) :=
  SnakeInput.isIso_δ _ h hs

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