Commit 2024-11-23 09:01 4fd77b8b

View on Github →

chore: missing MvPolynomial.eval lemmas (#19356) Revealed by a new user question on zulip.

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

added theorem MvPolynomial.aevalTower_ofNat

added theorem MvPolynomial.aeval_ofNat

added theorem MvPolynomial.eval_ofNat

added theorem MvPolynomial.eval₂_natCast

added theorem MvPolynomial.eval₂_ofNat