Commit 2021-01-07 10:05 9dd1496a

View on Github →

chore(group_theory/perm/basic): Add some missing simp lemmas (#5614) simp can't find the appropriate equiv lemmas as they are about refl not 1, even though those are defeq.

Estimated changes

Modified src/group_theory/perm/basic.lean

added theorem equiv.perm.inv_trans

added theorem equiv.perm.mul_refl

added theorem equiv.perm.mul_symm

added theorem equiv.perm.one_symm

added theorem equiv.perm.one_trans

added theorem equiv.perm.refl_inv

added theorem equiv.perm.refl_mul

added theorem equiv.perm.symm_mul

added theorem equiv.perm.trans_inv

added theorem equiv.perm.trans_one