Theorem pow_le_pow_of_le_one_aux

Modification history

2024-01-30 22:28
Mathlib/Algebra/GroupPower/Lemmas.lean
refactor: Delete `Algebra.GroupPower.Lemmas` (#9411) …
Deleted pow_le_pow_of_le_one_auxView on Github →
2022-12-19 11:23
Mathlib/Algebra/GroupPower/Lemmas.lean
feat port Algebra.GroupPower.Lemmas (#1055) …
Added pow_le_pow_of_le_one_auxView on Github →