Commit 2026-04-21 15:48 7e6661fc

View on Github →

chore(RingTheory/Localization): rename and generalize IsLocalization.at_units (#38084) We also move it from Localization.Defs to Localization.Basic.

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

added theorem Algebra.algebraMapSubmonoid_isUnit_le

modified theorem Algebra.algebraMapSubmonoid_powers

modified theorem Algebra.mem_algebraMapSubmonoid_of_mem

Modified Mathlib/RingTheory/LocalProperties/Basic.lean

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

added theorem IsLocalization.of_le_isUnit

added theorem IsLocalization.of_le_isUnit_of_bijective

Modified Mathlib/RingTheory/Localization/Defs.lean

deleted theorem IsLocalization.at_units

Modified Mathlib/RingTheory/Localization/FractionRing.lean