Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-16 23:59 3bf72416

View on Github →

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.

Estimated changes