mathlib

6b600207 - chore(group_theory/subgroup/basic): Protect `subgroup.subtype` (#18712)

chore(group_theory/subgroup/basic): Protect `subgroup.subtype` (#18712) and `subgroup_class.subtype`. This was breaking the `subtype` notation for me in #18684. The longer term fix would be to add a `_root_` in the notation declaration.