Theorem Algebra.FinitePresentation.of_isLocalizationAway

Modification history

2025-12-12 15:51
Mathlib/RingTheory/Localization/Away/AdjoinRoot.lean
feat(RingTheory): the etale locus of an algebra (#32529)
Added Algebra.FinitePresentation.of_isLocalizationAwayView on Github →