Theorem MvPolynomial.isPrime_idealOfVars

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.isPrime_idealOfVars View on Github →