isIso_δ_of_isZero — Mathlib

English

If H_{n+1}(G, X2) = 0 and H_n(G, X2) = 0, then δ hX (n+1) n rfl is an isomorphism.

Русский

Если H_{n+1}(G, X2) = 0 и H_n(G, X2) = 0, то δ hX (n+1) n rfl — изоморфизм.

LaTeX

$$$\mathrm{IsZero}\bigl(H_{n+1}(G, X_2)\bigr) \rightarrow \mathrm{IsZero}\bigl(H_n(G, X_2)\bigr) \rightarrow \mathrm{IsIso}\bigl(\delta hX (n+1) n rfl\bigr)$$$

Lean4

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

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