Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-30 06:17 09597669

View on Github →

chore(group_theory/quotient_group): open function, use rfl (#18014)

Estimated changes