mathlib

11d44d1a - feat(ring_theory/ideal): Add lift_of_right_inverse which is computable