Commit 2024-01-10 08:02 95e61f31

View on Github →

feat: define power-associativity in unital setting (#9439) introduce Prop-valued mixin NatPowAssoc and show that power-associativity holds for monoids.

Estimated changes

added theorem Int.cast_npow
added theorem Nat.cast_npow
added theorem npow_add
added theorem npow_mul'
added theorem npow_mul
added theorem npow_mul_assoc
added theorem npow_mul_comm
added theorem npow_one
added theorem npow_zero