Documentation
Provenance
.
Semirings
.
Nat
Search
return to top
source
Imports
Init
Provenance.SemiringWithMonus
Imported by
instSemiringWithMonusNat
instHasAltLinearOrderNat
Nat
.
mul_sub_left_distributive
Nat
.
not_idempotent
Nat
.
not_absorptive
source
instance
instSemiringWithMonusNat
:
SemiringWithMonus
ℕ
Equations
One or more equations did not get rendered due to their size.
source
instance
instHasAltLinearOrderNat
:
HasAltLinearOrder
ℕ
Equations
instHasAltLinearOrderNat
=
{
altOrder
:=
inferInstance
}
source
theorem
Nat
.
mul_sub_left_distributive
:
_root_.mul_sub_left_distributive
ℕ
source
theorem
Nat
.
not_idempotent
:
¬
idempotent
ℕ
source
theorem
Nat
.
not_absorptive
:
¬
absorptive
ℕ