Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-16 17:52 601f2ab7

View on Github →

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

Estimated changes

Modified src/ring_theory/ideal/basic.lean

modified theorem ideal.mem_infi

modified theorem ideal.mem_supr_of_mem