Theorem isLocalHom_iff_map_ringInverse

Modification history

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