Commit 2022-10-11 09:55 21926ffe
View on Github →feat(group_theory/subgroup/pointwise): Basic lemmas (#16856)
This PR adds some basic lemmas smul_bot, smul_inf, and smul_normal (a restatement of normal.conj_act in terms of mul_aut.conj).
feat(group_theory/subgroup/pointwise): Basic lemmas (#16856)
This PR adds some basic lemmas smul_bot, smul_inf, and smul_normal (a restatement of normal.conj_act in terms of mul_aut.conj).