Theorem MvPolynomial.fg_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.fg_idealOfVarsView on Github →