Commit 2025-11-27 13:47 9ea0d96e

View on Github →

feat(RingTheory): IsStandardEtale (#32138)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Bivariate.lean

deleted theorem Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial

deleted theorem Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial

added theorem Polynomial.Bivariate.pderiv_one_equivMvPolynomial

added theorem Polynomial.Bivariate.pderiv_zero_equivMvPolynomial

Modified Mathlib/RingTheory/Etale/Basic.lean

deleted theorem Algebra.FormallyEtale.Algebra.FormallyEtale.iff_of_surjective

deleted theorem Algebra.FormallyEtale.Algebra.FormallyEtale.of_restrictScalars

added theorem Algebra.FormallyEtale.iff_of_surjective

added theorem Algebra.FormallyEtale.of_restrictScalars

Modified Mathlib/RingTheory/Etale/StandardEtale.lean

added theorem Algebra.IsStandardEtale.of_equiv

added theorem Algebra.IsStandardEtale.of_isLocalizationAway

added theorem Algebra.IsStandardEtale.of_surjective

added theorem StandardEtalePresentation.aeval_val_equivMvPolynomial

added def StandardEtalePresentation.equivRing

added theorem StandardEtalePresentation.equivRing_symm_X

added theorem StandardEtalePresentation.equivRing_x

added theorem StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x

added def StandardEtalePresentation.mapEquiv

added def StandardEtalePresentation.toPresentation

added def StandardEtalePresentation.toSubmersivePresentation

added theorem StandardEtalePresentation.toSubmersivePresentation_jacobian

added structure StandardEtalePresentation

Modified Mathlib/RingTheory/Extension/Generators.lean

added theorem Algebra.Generators.ker_ofAlgHom