Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-02 14:44 dbb5ca1e

View on Github →

refactor(group_theory/perm): move perm.subtype_perm to basic (#6005) Both perm.subtype_perm and perm.of_subtype can be moved up the import hierarchy out of group_theory/perm/sign since they do not rely on any finiteness assumption.

Estimated changes