Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-16 13:27 39afa0b3

View on Github →

chore(*): remove after the fact attribute [irreducible] at several places (2) (#18180) Part of #18164, sequel to #18168.

Estimated changes