mathlib3

ae0f31c7 - feat(ring_theory/ideal/basic): allow noncommutativity in `span_singleton_mul_left_unit` (#18088)