feat(group_theory): computable 1st isomorphism theorem (#7988)
This PR defines a computable version of the first isomorphism theorem for groups and monoids that takes a right inverse of the map, `quotient_ker_equiv_of_right_inverse`.
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
