mathlib3

601f2ab7 - fix(ring_theory/ideal/basic): remove universe restriction (#10843)