Theorem pow_sub_of_lt

Modification history

2024-05-13 11:45
Mathlib/Algebra/GroupWithZero/Power.lean
chore: Delete `Algebra.GroupWithZero.Power` (#12825) …
Modified pow_sub_of_ltView on Github →
2023-01-19 07:45
Mathlib/Algebra/GroupWithZero/Power.lean
chore: format `by` line breaks (#1523) …
Modified pow_sub_of_ltView on Github →
2023-01-02 19:20
Mathlib/Algebra/GroupWithZero/Power.lean
feat: port algebra.group_with_zero.power (#1251) …
Added pow_sub_of_ltView on Github →