HepLean Documentation
Mathlib
.
Algebra
.
EuclideanDomain
.
Int
Search
Google site search
return to top
source
Imports
Init
Mathlib.Algebra.EuclideanDomain.Defs
Mathlib.Algebra.Ring.Int.Defs
Mathlib.Algebra.Order.Group.Unbundled.Int
Imported by
Int
.
euclideanDomain
Instances for Euclidean domains
#
Int.euclideanDomain
: shows that
ℤ
is a Euclidean domain.
source
instance
Int
.
euclideanDomain
:
EuclideanDomain
ℤ
Equations
One or more equations did not get rendered due to their size.