Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-22 14:57 6eb55641

View on Github →

chore(data/equiv/basic): Add a simp lemma perm.coe_mul (#4723) This mirrors equiv.coe_trans

Estimated changes

added theorem equiv.perm.coe_mul
modified theorem equiv.perm.mul_apply