Theorem Localization.AtPrime.algebraMap_eq

Modification history

2026-09-03 08:22

Mathlib/RingTheory/Localization/AtPrime/Basic.lean

refactor(RingTheory/Localization/AtPrime/Basic): replace `IsLiesOverAlgebra` with `IsScalarTower` (#41100) …

Added Localization.AtPrime.algebraMap_eq View on Github →