hasNoLoop_down'

Mathlib.Algebra.Homology.HasNoLoop

URI: https://scilib.ai/kg/mathlib#ComplexShape.hasNoLoop_down'

← MathLib Explorer

English

If Up'(a) has NoLoop, then Down'(a) has NoLoop as well.

Русский

Если Up'(a) не имеет петель, то и Down'(a) тоже не имеет петель.

LaTeX

$$$\text{Down}'(a).HasNoLoop$$$

Lean4

theorem hasNoLoop_down' {α : Type*} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α] (a : α) (ha : a ≠ 0) :
    (down' a).HasNoLoop := by
  have := hasNoLoop_up' a ha
  exact inferInstanceAs (up' a).symm.HasNoLoop

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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