Commit 2026-01-07 13:28 65544d47

View on Github →

feat(RingTheory): noetherian model for etale algebras (#32837)

Estimated changes

Modified Mathlib/RingTheory/Extension/Presentation/Core.lean

added theorem Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs

added theorem Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs

added def Algebra.SubmersivePresentation.coeffs

added theorem Algebra.SubmersivePresentation.coeffs_toPresentation_subset_coeffs

added theorem Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one

added theorem Algebra.SubmersivePresentation.finite_coeffs

added def Algebra.SubmersivePresentation.invJacobianOfHasCoeffs

added def Algebra.SubmersivePresentation.jacobianOfHasCoeffs

added def Algebra.SubmersivePresentation.jacobianRelations

added def Algebra.SubmersivePresentation.jacobianRelationsOfHasCoeffs

added theorem Algebra.SubmersivePresentation.jacobianRelations_spec

added theorem Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs

added theorem Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs

added theorem Algebra.SubmersivePresentation.map_jacobianRelationsOfHasCoeffs

added def Algebra.SubmersivePresentation.ofHasCoeffs

added theorem Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs

Modified Mathlib/RingTheory/Smooth/NoetherianDescent.lean

added theorem Algebra.Smooth.DescentAux.fg_subalgebra