Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-11 03:15 8c60a927

View on Github →

fix(ring_theory/algebraic): prove a diamond exists and remove the instances (#11935) It seems nothing used these instances anyway.

Estimated changes