mathlib3

21926ffe - 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`).