Commit 2023-12-27 08:00 4d78a650

View on Github →

chore(Perm/Basic): generalize swap_smul_involutive (#9180) Generalize Equiv.Perm.ModSumCongr.swap_smul_involutive to any action of Equiv.Perm _, move it to Perm/Basic.

Estimated changes

modified theorem Equiv.swap_mul_self_mul