Commit 2025-11-20 14:55 b26203fc

View on Github →

feat(RingTheory/Etale): standard etale maps (#30867)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/Bivariate.lean

added theorem Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial

added theorem Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial

added def Polynomial.Bivariate.equivMvPolynomial

added theorem Polynomial.Bivariate.equivMvPolynomial_C_C

added theorem Polynomial.Bivariate.equivMvPolynomial_C_X

added theorem Polynomial.Bivariate.equivMvPolynomial_X

added theorem Polynomial.Bivariate.equivMvPolynomial_symm_C

added theorem Polynomial.Bivariate.equivMvPolynomial_symm_X_0

added theorem Polynomial.Bivariate.equivMvPolynomial_symm_X_1

Modified Mathlib/Algebra/Polynomial/Taylor.lean

added theorem Polynomial.aeval_add_of_sq_eq_zero

Created Mathlib/RingTheory/Etale/StandardEtale.lean

added theorem StandardEtalePair.HasMap.isUnit_derivative_f

added theorem StandardEtalePair.HasMap.map

added def StandardEtalePair.HasMap

added theorem StandardEtalePair.aeval_X_g_mul_mk_X

added def StandardEtalePair.equivAwayAdjoinRoot

added def StandardEtalePair.equivAwayQuotient

added def StandardEtalePair.equivMvPolynomialQuotient

added theorem StandardEtalePair.equivMvPolynomialQuotient_symm_apply

added def StandardEtalePair.equivPolynomialQuotient

added theorem StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot

added theorem StandardEtalePair.hasMap_X

added def StandardEtalePair.homEquiv

added theorem StandardEtalePair.hom_ext

added theorem StandardEtalePair.inv_aeval_X_g

added def StandardEtalePair.lift

added theorem StandardEtalePair.lift_X

added theorem StandardEtalePair.lift_X_left

added structure StandardEtalePair

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

added theorem Ideal.quotientEquivAlg_mk

added theorem Ideal.quotientEquivAlg_symm