mathlib

24399402 - feat(group_theory/subgroup): Add lift_of_right_inverse which is computable