mathlib

3bf72416 - feat(algebra/algebra,linear_algebra): add *_equiv.of_left_inverse (#6167)

feat(algebra/algebra,linear_algebra): add *_equiv.of_left_inverse (#6167) The main purpose of this change is to add equivalences onto the range of a function with a left-inverse: * `algebra_equiv.of_left_inverse` * `linear_equiv.of_left_inverse` * `ring_equiv.of_left_inverse` * `ring_equiv.sof_left_inverse` (the sub***S***emiring version) This also: * Renames `alg_hom.alg_equiv.of_injective` to `alg_equiv.of_injective` * Adds `subalgebra.mem_range_self` and `subsemiring.mem_srange_self` for consistency with `subring.mem_range_self` * Replaces `subring.surjective_onto_range` with `subring.range_restrict_surjective`, which have defeq statements These are computable versions of `*_equiv.of_injective`, with the benefit of having a known inverse, and in the case of `linear_equiv` working for `semiring` and not just `ring`.