From c2d184046334aff5c03dba04614f8e248f0c1e78 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 9 Jul 2026 18:38:04 +0200 Subject: [PATCH] refactor(Algebra/Polynomial): make `coeff` return a `Finsupp` This matches `AddMonoidAlgebra`. --- Mathlib/Algebra/Polynomial/Basic.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Basic.lean b/Mathlib/Algebra/Polynomial/Basic.lean index 4f38dc96829bbb..62d009fa0cd19a 100644 --- a/Mathlib/Algebra/Polynomial/Basic.lean +++ b/Mathlib/Algebra/Polynomial/Basic.lean @@ -174,7 +174,6 @@ theorem ofFinsupp_smul {S : Type*} [SMulZeroClass S R] (a : S) (b) : (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X]) := rfl -set_option linter.style.whitespace false in -- manual alignment is not recognised @[simp] theorem ofFinsupp_pow (a) (n : ℕ) : (⟨a ^ n⟩ : R[X]) = ⟨a⟩ ^ n := by change _ = npowRec n _ @@ -560,13 +559,13 @@ theorem X_pow_mul_monomial (k n : ℕ) (r : R) : X ^ k * monomial n r = monomial rw [X_pow_mul, monomial_mul_X_pow] /-- `coeff p n` (often denoted `p.coeff n`) is the coefficient of `X^n` in `p`. -/ -def coeff : R[X] → ℕ → R +def coeff : R[X] → ℕ →₀ R | ⟨p⟩ => p.coeff @[simp] theorem coeff_ofFinsupp (p) : coeff (⟨p⟩ : R[X]) = p.coeff := by rw [coeff] -theorem coeff_injective : Injective (coeff : R[X] → ℕ → R) := by rintro ⟨p⟩ ⟨q⟩; simp [coeff] +theorem coeff_injective : Injective (coeff : R[X] → ℕ →₀ R) := by rintro ⟨p⟩ ⟨q⟩; simp [coeff] @[simp] theorem coeff_inj : p.coeff = q.coeff ↔ p = q :=