Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes