Commit 2020-12-16 15:31 39ecd1ab
View on Github →chore(group_theory/group_action/basic): Add a simp lemma about smul on quotient groups (#5374)
By pushing mk to the outside, this increases the chance they can cancel with an outer lift
chore(group_theory/group_action/basic): Add a simp lemma about smul on quotient groups (#5374)
By pushing mk to the outside, this increases the chance they can cancel with an outer lift