mono_δ_of_isZero

Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence

URI: https://scilib.ai/kg/mathlib#groupHomology.mono_δ_of_isZero

English

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

Русский

Если H_{n+1}(G, X2) = 0, то δ hX (n+1) n rfl — монообразное отображение.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru