Abs

📁 Source: Mathlib/Tactic/NormNum/Abs.lean

Statistics

Metric	Count
Definitions evalAbs	1
Theorems isNNRat_abs_neg, isNNRat_abs_nonneg, isNat_abs_neg, isNat_abs_nonneg	4
Total	5

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
evalAbs 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNNRat_abs_neg 📖	mathematical	IsRat DivisionRing.toRing	IsNNRat DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	Int.cast_negOfNat neg_mul abs_neg abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing mul_nonneg IsOrderedRing.toPosMulMono Nat.cast_nonneg' IsStrictOrderedRing.toZeroLEOneClass invOf_eq_inv PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
isNNRat_abs_nonneg 📖	mathematical	IsNNRat DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring	abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing	—	abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing mul_nonneg IsOrderedRing.toPosMulMono Nat.cast_nonneg' IsStrictOrderedRing.toZeroLEOneClass invOf_eq_inv PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
isNat_abs_neg 📖	mathematical	IsInt	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne abs AddGroupWithOne.toAddGroup	—	IsInt.out Int.cast_negOfNat abs_neg Nat.abs_cast
isNat_abs_nonneg 📖	mathematical	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	abs AddGroupWithOne.toAddGroup	—	IsNat.out Nat.abs_cast

---

← Back to Index