Theorem npow_mul_assoc

Modification history

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