Theorem npow_mul'

Modification history

2024-01-10 08:02
Mathlib/Algebra/Group/NatPowAssoc.lean
feat: define power-associativity in unital setting (#9439) …
Added npow_mul'View on Github →