chore(ring_theory/polynomial/basic): Generalize polynomial.degree_lt_equiv to commutative rings (#13190)

This is a minor PR to generalise degree_lt_equiv to comm_ring.
Its restriction to field appears to be an oversight.



Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>

Author: linesthatinterlace

src/ring_theory/polynomial/basic.lean

@@ -100,11 +100,11 @@ begin
   exact lt_of_le_of_lt (degree_X_pow_le _) (with_bot.coe_lt_coe.2 $ finset.mem_range.1 hk)
 end
 
-/-- The first `n` coefficients on `degree_lt n` form a linear equivalence with `fin n → F`. -/
-def degree_lt_equiv (F : Type*) [field F] (n : ℕ) : degree_lt F n ≃ₗ[F] (fin n → F) :=
-{ to_fun := λ p n, (↑p : F[X]).coeff n,
+/-- The first `n` coefficients on `degree_lt n` form a linear equivalence with `fin n → R`. -/
+def degree_lt_equiv (R : Type u) [comm_ring R] (n : ℕ) : degree_lt R n ≃ₗ[R] (fin n → R) :=
+{ to_fun := λ p n, (↑p : R[X]).coeff n,
   inv_fun := λ f, ⟨∑ i : fin n, monomial i (f i),
-    (degree_lt F n).sum_mem (λ i _, mem_degree_lt.mpr (lt_of_le_of_lt
+    (degree_lt R n).sum_mem (λ i _, mem_degree_lt.mpr (lt_of_le_of_lt
       (degree_monomial_le i (f i)) (with_bot.coe_lt_coe.mpr i.is_lt)))⟩,
   map_add' := λ p q, by { ext, rw [submodule.coe_add, coeff_add], refl },
   map_smul' := λ x p, by { ext, rw [submodule.coe_smul, coeff_smul], refl },