Commit 2026-09-30 20:39 2a885768

feat: add {IsUnit}.map_ringInverse (#44087) This adds Ring.inverse analogues of IsUnit.map and map_inv/map_inv₀. They are not marked simp to prevent expensive instance synthesis or unwanted simplification in contexts where ⁻¹ is preferred to ⁻¹ʳ.