Theorem npow_one

Modification history

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