Theorem npow_add

Modification history

2025-10-19 14:27
Mathlib/Algebra/Group/NatPowAssoc.lean
chore: miscellaneous linter whitespace fixes (#30663) …
Modified npow_addView on Github →
2024-01-10 08:02
Mathlib/Algebra/Group/NatPowAssoc.lean
feat: define power-associativity in unital setting (#9439) …
Added npow_addView on Github →