Commit 2025-02-25 22:29 6a854f21

View on Github →

feat: trivial lemmas about polynomial casts (#22227)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Basic.lean

added theorem Polynomial.ofFinsupp_intCast

added theorem Polynomial.ofFinsupp_natCast

added theorem Polynomial.ofFinsupp_ofNat

added theorem Polynomial.toFinsupp_intCast

added theorem Polynomial.toFinsupp_natCast

added theorem Polynomial.toFinsupp_ofNat