Theorem zpow_eq_pow
Modification history
2023-01-24 16:51
Mathlib/Algebra/Group/Defs.lean
fix: to_additive translates pow to nsmul (#1502) …
Modified zpow_eq_powView on Github →2023-01-09 17:24
Mathlib/Algebra/Group/Defs.lean
feat: improve the way to_additive deals with attributes (#1314) …
Modified zpow_eq_powView on Github →2022-11-25 16:23
Mathlib/Algebra/Group/Defs.lean
feat: improve `toAdditive.guessName` (#715) …
Modified zpow_eq_powView on Github →2022-11-24 08:51
Mathlib/Algebra/Group/Defs.lean
fix(Algebra/Group/Defs): make `to_additive` play nice with `pow` and `smul` (#706) …
Modified zpow_eq_powView on Github →