Theorem MvPolynomial.idealOfVars_fg

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)
Deleted MvPolynomial.idealOfVars_fgView on Github →
2026-03-04 10:55
Mathlib/RingTheory/MvPolynomial/Ideal.lean
feat(RingTheory): add some easy lemmas (#35789) …
Added MvPolynomial.idealOfVars_fgView on Github →