Theorem RingHom.finitePresentation_stableUnderBaseChange

Modification history

2024-11-06 16:11

Mathlib/RingTheory/RingHom/FinitePresentation.lean

refactor(CategoryTheory/MorphismProperty): turn `StableUnderBaseChange` into a class (#18692) …

Deleted RingHom.finitePresentation_stableUnderBaseChange View on Github →

2024-07-24 09:47

Mathlib/RingTheory/RingHom/FinitePresentation.lean

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

Added RingHom.finitePresentation_stableUnderBaseChange View on Github →