feat(ring_theory/polynomial/basic): prerequisites for galois_definiti…

…on (#4829)

Co-authored-by: Johan Commelin <johan@commelin.net>

src/data/polynomial/degree/basic.lean

@@ -235,6 +235,10 @@ lemma sum_over_range [add_comm_monoid S] (p : polynomial R) {f : ℕ → R → S
   p.sum f = ∑ (a : ℕ) in range (p.nat_degree + 1), f a (coeff p a) :=
 sum_over_range' p h (p.nat_degree + 1) (lt_add_one _)
 
+lemma as_sum_range' (p : polynomial R) (n : ℕ) (w : p.nat_degree < n) :
+  p = ∑ i in range n, monomial i (coeff p i) :=
+p.sum_single.symm.trans $ p.sum_over_range' (λ n, single_zero) _ w
+
 lemma as_sum_range (p : polynomial R) :
   p = ∑ i in range (p.nat_degree + 1), monomial i (coeff p i) :=
 p.sum_single.symm.trans $ p.sum_over_range $ λ n, single_zero

src/ring_theory/polynomial/basic.lean

@@ -23,7 +23,7 @@ import ring_theory.principal_ideal_domain
 import ring_theory.polynomial.content
 
 noncomputable theory
-open_locale classical
+open_locale classical big_operators
 
 universes u v w
 
@@ -96,6 +96,32 @@ 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 : polynomial F).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_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 },
+  left_inv :=
+  begin
+    rintro ⟨p, hp⟩, ext1,
+    simp only [submodule.coe_mk],
+    by_cases hp0 : p = 0,
+    { subst hp0, simp only [coeff_zero, linear_map.map_zero, finset.sum_const_zero] },
+    rw [mem_degree_lt, degree_eq_nat_degree hp0, with_bot.coe_lt_coe] at hp,
+    conv_rhs { rw [p.as_sum_range' n hp, ← fin.sum_univ_eq_sum_range] },
+  end,
+  right_inv :=
+  begin
+    intro f, ext i,
+    simp only [finset_sum_coeff, submodule.coe_mk],
+    rw [finset.sum_eq_single i, coeff_monomial, if_pos rfl],
+    { rintro j - hji, rw [coeff_monomial, if_neg], rwa [← subtype.ext_iff] },
+    { intro h, exact (h (finset.mem_univ _)).elim }
+  end }
+
 local attribute [instance] subset.ring
 
 /-- Given a polynomial, return the polynomial whose coefficients are in