Commit 2025-02-10 11:41 218aa7eb

feat: Add lemma mul_pow_mul (#21619) In a monoid (a * b) ^ n * a = a * (b * a) ^ n