mathlib

ba2d8fb3 - feat(ring_theory/ideal/operations): add span_singleton_mul_left lemmas (#18056)