Theorem MvPolynomial.aeval_one_tmul

Modification history

2024-09-18 11:42
Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
feat(RingTheory/StandardSmooth): base change of standard smooth algebras (#16853) …
Added MvPolynomial.aeval_one_tmulView on Github →