Basic
📁 Source: FLT/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
| 13 | |
| Total | 13 |
AbsoluteValue
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
eq_one_iff_of_lt_one_iff 📖 | — | — | — | — | eq_one_of_lt_one_iff |
eq_one_of_lt_one_iff 📖 | — | — | — | — | one_lt_iff_of_lt_one_iff |
inv_lt_one_iff 📖 | — | — | — | — | — |
inv_pos 📖 | — | — | — | — | — |
isNontrivial_iff_exists_abv_gt_one 📖 | — | — | — | — | ne_zero_of_lt_one |
mul_one_div_lt_iff 📖 | — | — | — | — | — |
mul_one_div_pow_lt_iff 📖 | — | — | — | — | mul_one_div_lt_iff |
ne_zero_of_lt_one 📖 | — | — | — | — | — |
one_add_pow_le 📖 | — | — | — | — | — |
one_lt_iff_of_lt_one_iff 📖 | — | — | — | — | one_lt_of_lt_one |
one_lt_of_lt_one 📖 | — | — | — | — | inv_lt_one_iffne_zero_of_lt_one |
one_sub_pow_le 📖 | — | — | — | — | — |
pos_of_pos 📖 | — | — | — | — | — |
---