hasNoLoop_up

Mathlib.Algebra.Homology.HasNoLoop

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\text{HasNoLoop}(Up) \, \text{for all appropriate } a$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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