Commit 2023-04-02 09:13 6b600207
View on Github →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.