feat(group_theory/subgroup/pointwise): Basic lemmas (#16856)
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`).





leanprover-community/mathlib,leanprover-community/mathlib