Theorem MvPolynomial.span_X_image_isPrime

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_isPrimeView on Github →