Commit 2024-06-12 10:07 c290d69e

View on Github →

feat(RingTheory): finite type and finite presentation are stable under base change (#13696)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/FiniteStability.lean

added theorem Algebra.FiniteType.baseChangeAux_surj

Modified Mathlib/RingTheory/RingHom/FiniteType.lean

added theorem RingHom.finiteType_stableUnderBaseChange

Modified Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

added theorem MvPolynomial.algebraTensorAlgEquiv_symm_X

added theorem MvPolynomial.algebraTensorAlgEquiv_symm_monomial

added theorem MvPolynomial.algebraTensorAlgEquiv_tmul