Commit 2025-02-23 23:50 f9a634b0

View on Github →

refactor: move Polynomial.coeffs and related results (#22225) Move Polynomial.coeffs and related results from Mathlib.RingTheory.Polynomial.Basic to Mathlib.Algebra.Polynomial.Basic as a preparation step to add results for Polynomial.lifts using Polynomial.coeffs. This is to avoid importing Mathlib.RingTheory.Polynomial.Basic in Mathlib.Algebra.Polynomial.Lifts.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Basic.lean

added theorem Polynomial.coeff_mem_coeffs

added def Polynomial.coeffs

added theorem Polynomial.coeffs_monomial

added theorem Polynomial.coeffs_one

added theorem Polynomial.coeffs_zero

added theorem Polynomial.mem_coeffs_iff

Modified Mathlib/RingTheory/Polynomial/Basic.lean

deleted theorem Polynomial.coeff_mem_coeffs

deleted def Polynomial.coeffs

deleted theorem Polynomial.coeffs_monomial

deleted theorem Polynomial.coeffs_one

deleted theorem Polynomial.coeffs_zero

deleted theorem Polynomial.mem_coeffs_iff