Documentation Verification Report

HasNoLoop

📁 Source: Mathlib/Algebra/Homology/HasNoLoop.lean

Statistics

Metric	Count
Definitions `HasNoLoop`	1
Theorems `not_rel_self`, `exists_distinct_next_or`, `exists_distinct_prev_or`, `hasNoLoop_down`, `hasNoLoop_down'`, `hasNoLoop_up`, `hasNoLoop_up'`, `instHasNoLoopIntDown`, `instHasNoLoopIntUp`, `instHasNoLoopNatDown`, `instHasNoLoopNatUp`, `instHasNoLoopSymm`, `not_rel_of_eq`, `not_rel_self`	14
Total	15

ComplexShape

Definitions

Name	Category	Theorems
`HasNoLoop` 📖	CompData	9 math math: `instHasNoLoopNatDown`, `instHasNoLoopIntDown`, `instHasNoLoopSymm`, `hasNoLoop_down'`, `hasNoLoop_up`, `hasNoLoop_down`, `hasNoLoop_up'`, `instHasNoLoopIntUp`, `instHasNoLoopNatUp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_distinct_next_or` 📖	mathematical	—	`Rel`	—	—
`exists_distinct_prev_or` 📖	mathematical	—	`Rel`	—	—
`hasNoLoop_down` 📖	mathematical	—	`HasNoLoop` `down` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`hasNoLoop_down'`
`hasNoLoop_down'` 📖	mathematical	—	`HasNoLoop` `down'` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`hasNoLoop_up'` `instHasNoLoopSymm`
`hasNoLoop_up` 📖	mathematical	—	`HasNoLoop` `up` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`hasNoLoop_up'`
`hasNoLoop_up'` 📖	mathematical	—	`HasNoLoop` `up'` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`add_left_cancel` `add_zero`
`instHasNoLoopIntDown` 📖	mathematical	—	`HasNoLoop` `down` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Int.instMonoid`	—	`hasNoLoop_down` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`instHasNoLoopIntUp` 📖	mathematical	—	`HasNoLoop` `up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Int.instMonoid`	—	`hasNoLoop_up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`instHasNoLoopNatDown` 📖	mathematical	—	`HasNoLoop` `down` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne`	—	`hasNoLoop_down` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`instHasNoLoopNatUp` 📖	mathematical	—	`HasNoLoop` `up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Nat.instOne`	—	`hasNoLoop_up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`instHasNoLoopSymm` 📖	mathematical	—	`HasNoLoop` `symm`	—	`not_rel_self`
`not_rel_of_eq` 📖	mathematical	—	`Rel`	—	`not_rel_self`
`not_rel_self` 📖	mathematical	—	`Rel`	—	`HasNoLoop.not_rel_self`

ComplexShape.HasNoLoop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_rel_self` 📖	mathematical	—	`ComplexShape.Rel`	—	—

---

← Back to Index