Theorem MvPolynomial.span_X_image_eq_ker_aeval_ite_mem

Modification history

2026-10-18 11:37
Mathlib/RingTheory/MvPolynomial/Ideal.lean
feat(MvPolynomial): ideal generated by indeterminates in a polynomial ring over a domain is prime (#41399)
Added MvPolynomial.span_X_image_eq_ker_aeval_ite_memView on Github →