Theorem MvPolynomial.eval₂_map_comp_C

Modification history

2025-12-09 15:53
Mathlib/Algebra/MvPolynomial/Eval.lean
feat(RingTheory): smooth algebras have smooth Noetherian models (#25143) …
Added MvPolynomial.eval₂_map_comp_CView on Github →