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