Theorem IsLocalization.of_le_isUnit

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_isUnitView on Github →