Theorem Algebra.algebraMapSubmonoid_isUnit_le

Modification history

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