Sqrt

📁 Source: Mathlib/Data/Nat/Sqrt.lean

Statistics

Metric	Count
Definitions	0
Theorems `add_one_sqrt_le_of_ne_zero`, `eq_sqrt`, `eq_sqrt'`, `exists_mul_self`, `exists_mul_self'`, `le_sqrt`, `le_sqrt'`, `le_sqrt_of_eq_mul`, `le_three_of_sqrt_eq_one`, `log2_two`, `lt_succ_sqrt`, `lt_succ_sqrt'`, `not_exists_sq`, `not_exists_sq'`, `iter_sq_le`, `lt_iter_succ_sq`, `sqrt_add_eq`, `sqrt_add_eq'`, `sqrt_eq`, `sqrt_eq'`, `sqrt_eq_zero`, `sqrt_le`, `sqrt_le'`, `sqrt_le_add`, `sqrt_le_self`, `sqrt_le_sqrt`, `sqrt_lt`, `sqrt_lt'`, `sqrt_lt_self`, `sqrt_mul_sqrt_lt_succ`, `sqrt_mul_sqrt_lt_succ'`, `sqrt_one`, `sqrt_pos`, `sqrt_succ_le_succ_sqrt`, `sqrt_two`, `sqrt_zero`, `succ_le_succ_sqrt`, `succ_le_succ_sqrt'`	38
Total	38

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_one_sqrt_le_of_ne_zero` 📖	—	—	—	—	`le_induction` `sqrt_two` `le_trans` `sqrt_succ_le_succ_sqrt`
`eq_sqrt` 📖	—	—	—	—	`le_antisymm` `le_sqrt` `sqrt_lt`
`eq_sqrt'` 📖	—	—	—	—	`eq_sqrt`
`exists_mul_self` 📖	—	—	—	—	`sqrt_eq`
`exists_mul_self'` 📖	—	—	—	—	`exists_mul_self`
`le_sqrt` 📖	—	—	—	—	`le_trans` `sqrt_le` `lt_of_le_of_lt` `lt_succ_sqrt`
`le_sqrt'` 📖	—	—	—	—	`le_sqrt`
`le_sqrt_of_eq_mul` 📖	—	—	—	—	`le_total` `le_sqrt`
`le_three_of_sqrt_eq_one` 📖	—	—	—	—	`sqrt_lt`
`log2_two` 📖	—	—	—	—	—
`lt_succ_sqrt` 📖	—	—	—	—	—
`lt_succ_sqrt'` 📖	—	—	—	—	`lt_succ_sqrt`
`not_exists_sq` 📖	—	—	—	—	—
`not_exists_sq'` 📖	—	—	—	—	`not_exists_sq`
`sqrt_add_eq` 📖	—	—	—	—	`le_antisymm` `sqrt_lt` `le_sqrt`
`sqrt_add_eq'` 📖	—	—	—	—	`sqrt_add_eq`
`sqrt_eq` 📖	—	—	—	—	`sqrt_add_eq`
`sqrt_eq'` 📖	—	—	—	—	`sqrt_add_eq'`
`sqrt_eq_zero` 📖	—	—	—	—	`sqrt_lt`
`sqrt_le` 📖	—	—	—	—	—
`sqrt_le'` 📖	—	—	—	—	`sqrt_le`
`sqrt_le_add` 📖	—	—	—	—	`lt_succ_sqrt`
`sqrt_le_self` 📖	—	—	—	—	`le_trans` `sqrt_le`
`sqrt_le_sqrt` 📖	—	—	—	—	`le_sqrt` `le_trans` `sqrt_le`
`sqrt_lt` 📖	—	—	—	—	—
`sqrt_lt'` 📖	—	—	—	—	—
`sqrt_lt_self` 📖	—	—	—	—	`sqrt_lt`
`sqrt_mul_sqrt_lt_succ` 📖	—	—	—	—	`sqrt_le`
`sqrt_mul_sqrt_lt_succ'` 📖	—	—	—	—	`sqrt_le'`
`sqrt_one` 📖	—	—	—	—	—
`sqrt_pos` 📖	—	—	—	—	`le_sqrt`
`sqrt_succ_le_succ_sqrt` 📖	—	—	—	—	`sqrt_lt` `sqrt_le_add`
`sqrt_two` 📖	—	—	—	—	`log2_two` `sqrt.iter.eq_1`
`sqrt_zero` 📖	—	—	—	—	—
`succ_le_succ_sqrt` 📖	—	—	—	—	`lt_succ_sqrt`
`succ_le_succ_sqrt'` 📖	—	—	—	—	`lt_succ_sqrt'`

Nat.sqrt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iter_sq_le` 📖	—	—	—	—	—
`lt_iter_succ_sq` 📖	—	—	—	—	—

---

← Back to Index