Commit 2025-10-28 15:18 34f670d7

View on Github →

feat(RingTheory/Finiteness): a finite and finitely presented algebra is finitely presented (#29781) We show that if S is finite as a module over R and finitely presented as an algebra over R, then it is finitely presented as a module over R.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Tower.lean

added def AlgEquiv.extendScalarsOfSurjective

added theorem AlgEquiv.extendScalarsOfSurjective_symm

added theorem AlgEquiv.restrictScalars_extendScalarsOfSurjective

added def AlgHom.extendScalarsOfSurjective

added theorem AlgHom.restrictScalars_extendScalarsOfSurjective

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added theorem Polynomial.aeval_X_left_eq_map

Created Mathlib/RingTheory/Finiteness/ModuleFinitePresentation.lean

added theorem Module.Finite.exists_free_surjective

added theorem Module.FinitePresentation.iff_finitePresentation_of_finite

added theorem Module.FinitePresentation.of_finite_of_finitePresentation

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified docs/references.bib