Euclidean

📁 Source: Mathlib/Algebra/Order/AbsoluteValue/Euclidean.lean

Statistics

Metric	Count
Definitions IsEuclidean	1
Theorems map_lt_map_iff, map_lt_map_iff', sub_mod_lt, abs_isEuclidean	4
Total	5

AbsoluteValue

Definitions

Name	Category	Theorems
IsEuclidean 📖	CompData	3 math math: abs_isEuclidean, Polynomial.cardPowDegree_isEuclidean, IsAdmissible.toIsEuclidean

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_isEuclidean 📖	mathematical	—	IsEuclidean Int.euclideanDomain Ring.toSemiring Int.instRing SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instLinearOrder abs Int.instIsStrictOrderedRing	—	Int.instIsStrictOrderedRing Int.abs_eq_natAbs

AbsoluteValue.IsEuclidean

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_lt_map_iff 📖	mathematical	AbsoluteValue.IsEuclidean	Preorder.toLT PartialOrder.toPreorder DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing AbsoluteValue.funLike EuclideanDomain.r	—	map_lt_map_iff'
map_lt_map_iff' 📖	mathematical	AbsoluteValue.IsEuclidean	Preorder.toLT PartialOrder.toPreorder DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing AbsoluteValue.funLike EuclideanDomain.r	—	—
sub_mod_lt 📖	mathematical	AbsoluteValue.IsEuclidean	Preorder.toLT PartialOrder.toPreorder DFunLike.coe AbsoluteValue CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing AbsoluteValue.funLike EuclideanDomain.instMod	—	map_lt_map_iff EuclideanDomain.mod_lt

---

← Back to Index