Commit 2021-02-16 23:59 3bf72416

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 subSemiring 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.