Mathlib Changelog
v4
Changelog
About
Github
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