NatAbs

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

Statistics

Metric	Count
Definitions natAbsHom	1
Theorems natAbsHom_apply, natAbs_natCast_sub_natCast_of_ge, natAbs_natCast_sub_natCast_of_le	3
Total	4

Int

Definitions

Name	Category	Theorems
natAbsHom 📖	CompOp	1 math math: natAbsHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natAbsHom_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring instSemiring Nat.instMulZeroOneClass MonoidWithZeroHom.funLike natAbsHom	—	—
natAbs_natCast_sub_natCast_of_ge 📖	—	—	—	—	—
natAbs_natCast_sub_natCast_of_le 📖	—	—	—	—	—

---

← Back to Index