Field

Statistics

Metric	Count
Definitions	0
Theorems `eq_rpow_iff_lt_one_iff`, `exists_lt_one_one_le_of_ne_rpow`, `exists_one_lt_lt_one_of_ne_rpow`, `exists_rpow_of_one_lt`, `log_div_image_eq_singleton_of_le_one_iff`, `lt_one_iff_of_lt_one_imp`, `ne_pow_symm`	7
Total	7

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_rpow_iff_lt_one_iff` 📖	—	—	—	—	`exists_rpow_of_one_lt` `eq_one_iff_of_lt_one_iff` `inv_lt_one_iff`
`exists_lt_one_one_le_of_ne_rpow` 📖	—	—	—	—	`eq_rpow_iff_lt_one_iff` `lt_one_iff_of_lt_one_imp`
`exists_one_lt_lt_one_of_ne_rpow` 📖	—	—	—	—	`exists_lt_one_one_le_of_ne_rpow` `ne_pow_symm` `pos_of_pos`
`exists_rpow_of_one_lt` 📖	—	—	—	—	`log_div_image_eq_singleton_of_le_one_iff` `one_lt_iff_of_lt_one_iff`
`log_div_image_eq_singleton_of_le_one_iff` 📖	—	—	—	—	`one_lt_iff_of_lt_one_iff`
`lt_one_iff_of_lt_one_imp` 📖	—	—	—	—	`mul_one_div_pow_lt_iff` `pos_of_pos`
`ne_pow_symm` 📖	—	—	—	—	—

---