Theorem Localization.awayLift_mk

Modification history

2025-04-11 17:23

Mathlib/RingTheory/Localization/Away/Basic.lean

feat: generalize rest of Mathlib.RingTheory (#23194) …

Modified Localization.awayLift_mk View on Github →

2024-11-20 19:44

Mathlib/RingTheory/Localization/Away/Basic.lean

feat(AlgebraicGeometry): Proj is separated (#19290) …

Added Localization.awayLift_mk View on Github →