Theorem Nat.cast_npow

Modification history

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