Theorem MvPolynomial.aeval_ite_mem_eq

Modification history

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