mathlib

5e194d48 - feat(algebra/invertible): `map_inv_of` and some other basic results (#16202)

feat(algebra/invertible): `map_inv_of` and some other basic results (#16202) The titular lemma states that under suitable conditions, `f (⅟r) = ⅟(f r)`. This also provides some lemmas about left inverses, which are motivated primarily by proving `is_unit (algebra_map R (exterior_algebra R M) r) ↔ is_unit r`.