Theorem Polynomial.coeff_restriction'

Modification history

2026-11-02 08:15

Mathlib/RingTheory/Polynomial/Basic.lean

refactor(Algebra/Polynomial): make into an `abbrev` of `AddMonoidAlgebra` (#41981) …

Modified Polynomial.coeff_restriction'View on Github →

2025-01-16 11:16

Mathlib/RingTheory/Polynomial/Basic.lean

chore: survey of simp porting notes (#20787) …

Modified Polynomial.coeff_restriction'View on Github →

2023-03-30 13:14

Mathlib/RingTheory/Polynomial/Basic.lean

feat: port RingTheory.Polynomial.Basic (#3067)

Added Polynomial.coeff_restriction'View on Github →