mathlib

5a72dafd - feat(data/equiv/basic): add a computable version of equiv.set.range (#6821)

feat(data/equiv/basic): add a computable version of equiv.set.range (#6821) If a left-inverse of `f` is known, it can be used to construct the equiv both computably and with control over definitional reduction. This adds the definition `equiv.set.range_of_left_inverse` to mirror `linear_equiv.of_left_inverse` and `ring_equiv.of_left_inverse`.