hasNoLoop_down

Mathlib.Algebra.Homology.HasNoLoop

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

← MathLib Explorer

English

For any a with appropriate properties, Down(a) has NoLoop.

Русский

Для любого a с подходящими свойствами Down(a) имеет без петли.

LaTeX

$$$\text{HasNoLoop}(Down) \;\text{for all appropriate } a$$$

Lean4

theorem hasNoLoop_down {α : Type*} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α] [One α]
    (ha : (1 : α) ≠ 0) : (down α).HasNoLoop :=
  hasNoLoop_down' _ ha

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

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

Разделы

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

Аффилиация

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