Commit 2024-07-24 09:47 a6e9d0c8

View on Github →

feat(RingTheory): being finitely-presented is local (#15073)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

Created Mathlib/RingTheory/RingHom/FinitePresentation.lean

added theorem RingHom.finitePresentation_holdsForLocalizationAway

added theorem RingHom.finitePresentation_isLocal

added theorem RingHom.finitePresentation_localizationPreserves

added theorem RingHom.finitePresentation_ofLocalizationSpanTarget

added theorem RingHom.finitePresentation_ofLocalizationSpanTarget_aux

added theorem RingHom.finitePresentation_respectsIso

added theorem RingHom.finitePresentation_stableUnderBaseChange

added theorem RingHom.finitePresentation_stableUnderComposition