Lemmas

Statistics

Metric	Count
Definitions	0
Theorems `abs_le_sqrt`, `abs_le_sqrt_iff_sq_le`, `natAbs_eq_iff_mul_self_eq`, `natAbs_le_iff_mul_self_le`, `natAbs_lt_iff_mul_self_lt`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_le_sqrt` 📖	mathematical	—	`abs` `instLatticeInt` `instAddGroup` `sqrt`	—	`abs_mul_abs_self` `abs_nonneg` `instAddLeftMono` `covariant_swap_add_of_covariant_add` `sqrt_natCast` `Nat.cast_le` `instZeroLEOneClass` `instCharZero` `Nat.le_sqrt`
`abs_le_sqrt_iff_sq_le` 📖	mathematical	—	`abs` `instLatticeInt` `instAddGroup` `sqrt` `Monoid.toNatPow` `instMonoid`	—	`abs_le_sqrt` `pow_two`
`natAbs_eq_iff_mul_self_eq` 📖	—	—	—	—	`abs_eq_iff_mul_self_eq` `instIsStrictOrderedRing` `abs_eq_natAbs`
`natAbs_le_iff_mul_self_le` 📖	—	—	—	—	`abs_le_iff_mul_self_le` `instIsStrictOrderedRing` `abs_eq_natAbs`
`natAbs_lt_iff_mul_self_lt` 📖	—	—	—	—	`abs_lt_iff_mul_self_lt` `instIsStrictOrderedRing` `abs_eq_natAbs`

---