Commit 2026-10-18 11:37 bbeef912

View on Github →

feat(MvPolynomial): ideal generated by indeterminates in a polynomial ring over a domain is prime (#41399)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Variables.lean

added theorem MvPolynomial.aeval_ite_mem_eq

Modified Mathlib/RingTheory/AdicCompletion/Completeness.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

modified theorem RingHom.ker_isPrime

Modified Mathlib/RingTheory/MvPolynomial/Ideal.lean

added theorem MvPolynomial.fg_idealOfVars

deleted theorem MvPolynomial.idealOfVars_fg

added theorem MvPolynomial.isPrime_idealOfVars

added theorem MvPolynomial.span_X_image_eq_ker_aeval_ite_mem

added theorem MvPolynomial.span_X_image_isPrime