Theorem Algebra.algebraMapSubmonoid_powers

Modification history

2026-04-21 15:48
Mathlib/Algebra/Algebra/Basic.lean
chore(RingTheory/Localization): rename and generalize `IsLocalization.at_units` (#38084) …
Modified Algebra.algebraMapSubmonoid_powersView on Github →
2025-05-21 12:47
Mathlib/Algebra/Algebra/Basic.lean
feat(RingTheory/LocalProperties): constructor for `RingHom.OfLocalizationSpan` (#22933) …
Added Algebra.algebraMapSubmonoid_powersView on Github →