mathlib3

5456d487 - feat(ring_theory/ideal/basic): add ideal.span_pair lemmas (#18036)