Theorem map_inv_eq_ringInverse_map

Modification history

2026-09-30 20:39
Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean
feat: add `{IsUnit}.map_ringInverse` (#44087) …
Added map_inv_eq_ringInverse_mapView on Github →