Mathlib v3 is deprecated. Go to Mathlib v4

Theorem right.pow_lt_one_of_lt

Modification history

2022-08-24 07:00
src/algebra/group_power/order.lean
chore(algebra/order/with_zero): Move unrelated lemmas (#15676) …
Modified right.pow_lt_one_of_ltView on Github →
2022-01-28 16:51
src/algebra/order/with_zero.lean
refactor(algebra/linear_ordered_comm_group_with_zero, *): mostly take advantage of the new classes for `linear_ordered_comm_group_with_zero` (#7645) …
Added right.pow_lt_one_of_ltView on Github →