Theorem IsLocalization.of_le_isUnit_of_bijective

Modification history

2026-04-21 15:48
Mathlib/RingTheory/Localization/Basic.lean
chore(RingTheory/Localization): rename and generalize `IsLocalization.at_units` (#38084) …
Added IsLocalization.of_le_isUnit_of_bijectiveView on Github →