Commit 2021-03-25 03:23 5a72dafd

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.