Commit 2024-01-08 12:05 4f952160

View on Github →

chore: Move (r • x) ^ n = r ^ n • x ^ n earlier (#9502) Part of #9411

Estimated changes

deleted theorem smul_pow'
deleted theorem smul_pow
added theorem smul_pow'
added theorem smul_pow