HepLean Documentation
Mathlib
.
Algebra
.
Group
.
Nat
.
Units
Search
Google site search
return to top
source
Imports
Init
Mathlib.Logic.Unique
Mathlib.Algebra.Group.Nat.Basic
Mathlib.Algebra.Group.Units.Defs
Imported by
Nat
.
units_eq_one
Nat
.
addUnits_eq_zero
Nat
.
isUnit_iff
Nat
.
unique_units
Nat
.
unique_addUnits
The unit of the natural numbers
#
Units
#
source
theorem
Nat
.
units_eq_one
(u :
ℕ
ˣ
)
:
u
=
1
source
theorem
Nat
.
addUnits_eq_zero
(u :
AddUnits
ℕ
)
:
u
=
0
source
@[simp]
theorem
Nat
.
isUnit_iff
{n :
ℕ
}
:
IsUnit
n
↔
n
=
1
source
instance
Nat
.
unique_units
:
Unique
ℕ
ˣ
Equations
Nat.unique_units
=
{
default
:=
1
,
uniq
:=
Nat.units_eq_one
}
source
instance
Nat
.
unique_addUnits
:
Unique
(
AddUnits
ℕ
)
Equations
Nat.unique_addUnits
=
{
default
:=
0
,
uniq
:=
Nat.addUnits_eq_zero
}