AbsoluteValue

📁 Source: Mathlib/Data/Int/AbsoluteValue.lean

Statistics

Metric	Count
Definitions	0
Theorems map_units_int, map_units_intCast, map_units_int_smul	3
Total	3

AbsoluteValue

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_units_int 📖	mathematical	—	DFunLike.coe AbsoluteValue Int.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder funLike Units.val Int.instMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Int.units_eq_one_or map_one IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE Int.instNontrivial AddGroupSeminormClass.map_neg_eq_map MulRingSeminormClass.toAddGroupSeminormClass MulRingNormClass.toMulRingSeminormClass instMulRingNormClassOfNontrivialOfIsDomain IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.noZeroDivisors
map_units_intCast 📖	mathematical	—	DFunLike.coe AbsoluteValue Ring.toSemiring CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder funLike AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Units.val Int.instMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne CommRing.toRing	—	Int.units_eq_one_or Int.cast_one map_one IsStrictOrderedRing.isDomain AddGroup.existsAddOfLE Int.cast_neg AddGroupSeminormClass.map_neg_eq_map MulRingSeminormClass.toAddGroupSeminormClass MulRingNormClass.toMulRingSeminormClass instMulRingNormClassOfNontrivialOfIsDomain IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.noZeroDivisors
map_units_int_smul 📖	mathematical	—	DFunLike.coe AbsoluteValue Ring.toSemiring CommSemiring.toSemiring CommRing.toCommSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder funLike Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	Int.units_eq_one_or one_smul Units.neg_smul map_neg IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.noZeroDivisors AddGroup.existsAddOfLE

---

← Back to Index