Documentation
Mathlib
.
Data
.
Nat
.
Units
Search
Google site search
Mathlib
.
Data
.
Nat
.
Units
source
Imports
Init
Mathlib.Algebra.Group.Units
Mathlib.Data.Nat.Basic
Imported by
Nat
.
units_eq_one
Nat
.
addUnits_eq_zero
Nat
.
isUnit_iff
Nat
.
unique_units
Nat
.
unique_addUnits
The units of the natural numbers as a
Monoid
and
AddMonoid
#
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
ℕ
ˣ
source
instance
Nat
.
unique_addUnits
:
Unique
(
AddUnits
ℕ
)