Theorem pow_mul_comm'
Modification history
2020-09-10 14:56
src/algebra/group_power/basic.lean
chore(*): update to Lean 3.20.0c, account for nat.pow removal from core (#3985) …
Modified pow_mul_comm'View on Github →2020-06-08 17:34
src/algebra/group_power.lean
refactor(algebra/*): move `commute` below `ring` in `import`s (#2973) …
Modified pow_mul_comm'View on Github →