Theorem Int.cast_npow

Modification history

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