Nat

📁 Source: Mathlib/Algebra/Order/Ring/Nat.lean

Statistics

Metric	Count
Definitions instLinearOrderedCommMonoidWithZero	1
Theorems instIsStrictOrderedRing, isCompl_even_odd	2
Total	3

Nat

Definitions

Name	Category	Theorems
instLinearOrderedCommMonoidWithZero 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsStrictOrderedRing 📖	mathematical	—	IsStrictOrderedRing instSemiring instPartialOrder	—	instIsOrderedCancelAddMonoid instZeroLEOneClass instNontrivial
isCompl_even_odd 📖	mathematical	—	IsCompl Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra Set.instBoundedOrder setOf Even Odd instSemiring	—	—

---

← Back to Index