feat(*): localized R[X] notation for polynomial R (#11895)

I did not change `polynomial (complex_term_here taking args)` in many places because I thought it would be more confusing. Also, in some files that prove things about polynomials incidentally, I also did not include the notation and change the files.



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

archive/100-theorems-list/16_abel_ruffini.lean

@@ -24,13 +24,14 @@ Then all that remains is the construction of a specific polynomial satisfying th
 namespace abel_ruffini
 
 open function polynomial polynomial.gal ideal
+open_locale polynomial
 
 local attribute [instance] splits_ℚ_ℂ
 
 variables (R : Type*) [comm_ring R] (a b : ℕ)
 
 /-- A quintic polynomial that we will show is irreducible -/
-noncomputable def Φ : polynomial R := X ^ 5 - C ↑a * X + C ↑b
+noncomputable def Φ : R[X] := X ^ 5 - C ↑a * X + C ↑b
 
 variables {R}
 

src/algebra/algebra/spectrum.lean

@@ -85,6 +85,7 @@ begin
 end
 
 namespace spectrum
+open_locale polynomial
 
 section scalar_ring
 
@@ -134,7 +135,7 @@ begin
   rw [h_eq, ←smul_sub, is_unit_smul_iff],
 end
 
-open_locale pointwise
+open_locale pointwise polynomial
 
 theorem unit_smul_eq_smul (a : A) (r : Rˣ) :
   σ (r • a) = r • σ a :=
@@ -247,7 +248,7 @@ open polynomial
 /-- Half of the spectral mapping theorem for polynomials. We prove it separately
 because it holds over any field, whereas `spectrum.map_polynomial_aeval_of_degree_pos` and
 `spectrum.map_polynomial_aeval_of_nonempty` need the field to be algebraically closed. -/
-theorem subset_polynomial_aeval (a : A) (p : polynomial 𝕜) :
+theorem subset_polynomial_aeval (a : A) (p : 𝕜[X]) :
   (λ k, eval k p) '' (σ a) ⊆ σ (aeval a p) :=
 begin
   rintros _ ⟨k, hk, rfl⟩,
@@ -262,7 +263,7 @@ begin
   simpa only [aeval_X, aeval_C, alg_hom.map_sub] using hk,
 end
 
-lemma exists_mem_of_not_is_unit_aeval_prod {p : polynomial 𝕜} {a : A} (hp : p ≠ 0)
+lemma exists_mem_of_not_is_unit_aeval_prod {p : 𝕜[X]} {a : A} (hp : p ≠ 0)
   (h : ¬is_unit (aeval a (multiset.map (λ (x : 𝕜), X - C x) p.roots).prod)) :
   ∃ k : 𝕜, k ∈ σ a ∧ eval k p = 0 :=
 begin
@@ -277,7 +278,7 @@ end
 /-- The *spectral mapping theorem* for polynomials.  Note: the assumption `degree p > 0`
 is necessary in case `σ a = ∅`, for then the left-hand side is `∅` and the right-hand side,
 assuming `[nontrivial A]`, is `{k}` where `p = polynomial.C k`. -/
-theorem map_polynomial_aeval_of_degree_pos [is_alg_closed 𝕜] (a : A) (p : polynomial 𝕜)
+theorem map_polynomial_aeval_of_degree_pos [is_alg_closed 𝕜] (a : A) (p : 𝕜[X])
   (hdeg : 0 < degree p) : σ (aeval a p) = (λ k, eval k p) '' (σ a) :=
 begin
   /- handle the easy direction via `spectrum.subset_polynomial_aeval` -/
@@ -302,7 +303,7 @@ end
 /-- In this version of the spectral mapping theorem, we assume the spectrum
 is nonempty instead of assuming the degree of the polynomial is positive. Note: the
 assumption `[nontrivial A]` is necessary for the same reason as in `spectrum.zero_eq`. -/
-theorem map_polynomial_aeval_of_nonempty [is_alg_closed 𝕜] [nontrivial A] (a : A) (p : polynomial 𝕜)
+theorem map_polynomial_aeval_of_nonempty [is_alg_closed 𝕜] [nontrivial A] (a : A) (p : 𝕜[X])
   (hnon : (σ a).nonempty) : σ (aeval a p) = (λ k, eval k p) '' (σ a) :=
 begin
   refine or.elim (le_or_gt (degree p) 0) (λ h, _) (map_polynomial_aeval_of_degree_pos a p),

src/algebra/cubic_discriminant.lean

@@ -39,6 +39,7 @@ noncomputable theory
 namespace cubic
 
 open cubic polynomial
+open_locale polynomial
 
 variables {R S F K : Type*}
 
@@ -51,7 +52,7 @@ section basic
 variables {P : cubic R} [semiring R]
 
 /-- Convert a cubic polynomial to a polynomial. -/
-def to_poly (P : cubic R) : polynomial R := C P.a * X ^ 3 + C P.b * X ^ 2 + C P.c * X + C P.d
+def to_poly (P : cubic R) : R[X] := C P.a * X ^ 3 + C P.b * X ^ 2 + C P.c * X + C P.d
 
 /-! ### Coefficients -/
 
@@ -131,7 +132,7 @@ end coeff
 section degree
 
 /-- The equivalence between cubic polynomials and polynomials of degree at most three. -/
-@[simps] def equiv : cubic R ≃ {p : polynomial R // p.degree ≤ 3} :=
+@[simps] def equiv : cubic R ≃ {p : R[X] // p.degree ≤ 3} :=
 { to_fun    := λ P, ⟨P.to_poly, degree_cubic_le⟩,
   inv_fun   := λ f, ⟨coeff f 3, coeff f 2, coeff f 1, coeff f 0⟩,
   left_inv  := λ P, by ext; simp only [subtype.coe_mk, coeffs],
@@ -140,7 +141,7 @@ section degree
     ext (_ | _ | _ | _ | n); simp only [subtype.coe_mk, coeffs],
     have h3 : 3 < n + 4 := by linarith only,
     rw [coeff_gt_three _ h3,
-        (degree_le_iff_coeff_zero (f : polynomial R) 3).mp f.2 _ $ with_bot.coe_lt_coe.mpr h3]
+        (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2 _ $ with_bot.coe_lt_coe.mpr h3]
   end }
 
 lemma degree (ha : P.a ≠ 0) : P.to_poly.degree = 3 := degree_cubic ha

src/algebra/linear_recurrence.lean

@@ -37,7 +37,7 @@ properties of eigenvalues and eigenvectors.
 
 noncomputable theory
 open finset
-open_locale big_operators
+open_locale big_operators polynomial
 
 /-- A "linear recurrence relation" over a commutative semiring is given by its
   order `n` and `n` coefficients. -/
@@ -183,7 +183,7 @@ variables {α : Type*} [comm_ring α] (E : linear_recurrence α)
 
 /-- The characteristic polynomial of `E` is
 `X ^ E.order - ∑ i : fin E.order, (E.coeffs i) * X ^ i`. -/
-def char_poly : polynomial α :=
+def char_poly : α[X] :=
   polynomial.monomial E.order 1 - (∑ i : fin E.order, polynomial.monomial i (E.coeffs i))
 
 /-- The geometric sequence `q^n` is a solution of `E` iff

src/algebra/polynomial/big_operators.lean

@@ -26,7 +26,7 @@ Recall that `∑` and `∏` are notation for `finset.sum` and `finset.prod` resp
 open finset
 open multiset
 
-open_locale big_operators
+open_locale big_operators polynomial
 
 universes u w
 
@@ -38,21 +38,21 @@ variables (s : finset ι)
 
 section semiring
 
-variables {α : Type*} [semiring α]
+variables {S : Type*} [semiring S]
 
-lemma nat_degree_list_sum_le (l : list (polynomial α)) :
+lemma nat_degree_list_sum_le (l : list S[X]) :
   nat_degree l.sum ≤ (l.map nat_degree).foldr max 0 :=
 list.sum_le_foldr_max nat_degree (by simp) nat_degree_add_le _
 
-lemma nat_degree_multiset_sum_le (l : multiset (polynomial α)) :
+lemma nat_degree_multiset_sum_le (l : multiset S[X]) :
   nat_degree l.sum ≤ (l.map nat_degree).foldr max max_left_comm 0 :=
 quotient.induction_on l (by simpa using nat_degree_list_sum_le)
 
-lemma nat_degree_sum_le (f : ι → polynomial α) :
+lemma nat_degree_sum_le (f : ι → S[X]) :
   nat_degree (∑ i in s, f i) ≤ s.fold max 0 (nat_degree ∘ f) :=
 by simpa using nat_degree_multiset_sum_le (s.val.map f)
 
-lemma degree_list_sum_le (l : list (polynomial α)) :
+lemma degree_list_sum_le (l : list S[X]) :
   degree l.sum ≤ (l.map nat_degree).maximum :=
 begin
   by_cases h : l.sum = 0,
@@ -68,23 +68,23 @@ begin
     simp [h] }
 end
 
-lemma nat_degree_list_prod_le (l : list (polynomial α)) :
+lemma nat_degree_list_prod_le (l : list S[X]) :
   nat_degree l.prod ≤ (l.map nat_degree).sum :=
 begin
   induction l with hd tl IH,
   { simp },
   { simpa using nat_degree_mul_le.trans (add_le_add_left IH _) }
 end
 
-lemma degree_list_prod_le (l : list (polynomial α)) :
+lemma degree_list_prod_le (l : list S[X]) :
   degree l.prod ≤ (l.map degree).sum :=
 begin
   induction l with hd tl IH,
   { simp },
   { simpa using (degree_mul_le _ _).trans (add_le_add_left IH _) }
 end
 
-lemma coeff_list_prod_of_nat_degree_le (l : list (polynomial α)) (n : ℕ)
+lemma coeff_list_prod_of_nat_degree_le (l : list S[X]) (n : ℕ)
   (hl : ∀ p ∈ l, nat_degree p ≤ n) :
   coeff (list.prod l) (l.length * n) = (l.map (λ p, coeff p n)).prod :=
 begin
@@ -111,7 +111,7 @@ end
 end semiring
 
 section comm_semiring
-variables [comm_semiring R] (f : ι → polynomial R) (t : multiset (polynomial R))
+variables [comm_semiring R] (f : ι → R[X]) (t : multiset R[X])
 
 lemma nat_degree_multiset_prod_le :
   t.prod.nat_degree ≤ (t.map nat_degree).sum :=
@@ -211,7 +211,7 @@ begin
   simpa using coeff_list_prod_of_nat_degree_le _ _ hl
 end
 
-lemma coeff_prod_of_nat_degree_le (f : ι → polynomial R) (n : ℕ)
+lemma coeff_prod_of_nat_degree_le (f : ι → R[X]) (n : ℕ)
   (h : ∀ p ∈ s, nat_degree (f p) ≤ n) :
   coeff (∏ i in s, f i) (s.card * n) = ∏ i in s, coeff (f i) n :=
 begin
@@ -275,7 +275,7 @@ by simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using
 end comm_ring
 
 section no_zero_divisors
-variables [comm_ring R] [no_zero_divisors R] (f : ι → polynomial R) (t : multiset (polynomial R))
+variables [comm_ring R] [no_zero_divisors R] (f : ι → R[X]) (t : multiset R[X])
 
 /--
 The degree of a product of polynomials is equal to
@@ -292,8 +292,8 @@ begin
   intros x hx, simp [h x hx]
 end
 
-lemma nat_degree_multiset_prod [nontrivial R] (s : multiset (polynomial R))
-  (h : (0 : polynomial R) ∉ s) :
+lemma nat_degree_multiset_prod [nontrivial R] (s : multiset R[X])
+  (h : (0 : R[X]) ∉ s) :
   nat_degree s.prod = (s.map nat_degree).sum :=
 begin
   rw nat_degree_multiset_prod',

src/algebra/polynomial/group_ring_action.lean

@@ -17,6 +17,7 @@ This file contains instances and definitions relating `mul_semiring_action` to `
 
 variables (M : Type*) [monoid M]
 
+open_locale polynomial
 namespace polynomial
 
 variables (R : Type*) [semiring R]
@@ -27,7 +28,7 @@ lemma smul_eq_map [mul_semiring_action M R] (m : M) :
   ((•) m) = map (mul_semiring_action.to_ring_hom M R m) :=
 begin
   suffices :
-    distrib_mul_action.to_add_monoid_hom (polynomial R) m =
+    distrib_mul_action.to_add_monoid_hom R[X] m =
       (map_ring_hom (mul_semiring_action.to_ring_hom M R m)).to_add_monoid_hom,
   { ext1 r, exact add_monoid_hom.congr_fun this r, },
   ext n r : 2,
@@ -37,7 +38,7 @@ end
 
 variables (M)
 
-noncomputable instance [mul_semiring_action M R] : mul_semiring_action M (polynomial R) :=
+noncomputable instance [mul_semiring_action M R] : mul_semiring_action M R[X] :=
 { smul := (•),
   smul_one := λ m, (smul_eq_map R m).symm ▸ map_one (mul_semiring_action.to_ring_hom M R m),
   smul_mul := λ m p q, (smul_eq_map R m).symm ▸ map_mul (mul_semiring_action.to_ring_hom M R m),
@@ -47,12 +48,12 @@ variables {M R}
 
 variables [mul_semiring_action M R]
 
-@[simp] lemma smul_X (m : M) : (m • X : polynomial R) = X :=
+@[simp] lemma smul_X (m : M) : (m • X : R[X]) = X :=
 (smul_eq_map R m).symm ▸ map_X _
 
 variables (S : Type*) [comm_semiring S] [mul_semiring_action M S]
 
-theorem smul_eval_smul (m : M) (f : polynomial S) (x : S) :
+theorem smul_eval_smul (m : M) (f : S[X]) (x : S) :
   (m • f).eval (m • x) = m • f.eval x :=
 polynomial.induction_on f
   (λ r, by rw [smul_C, eval_C, eval_C])
@@ -62,11 +63,11 @@ polynomial.induction_on f
 
 variables (G : Type*) [group G]
 
-theorem eval_smul' [mul_semiring_action G S] (g : G) (f : polynomial S) (x : S) :
+theorem eval_smul' [mul_semiring_action G S] (g : G) (f : S[X]) (x : S) :
   f.eval (g • x) = g • (g⁻¹ • f).eval x :=
 by rw [← smul_eval_smul, smul_inv_smul]
 
-theorem smul_eval [mul_semiring_action G S] (g : G) (f : polynomial S) (x : S) :
+theorem smul_eval [mul_semiring_action G S] (g : G) (f : S[X]) (x : S) :
   (g • f).eval x = g • f.eval (g⁻¹ • x) :=
 by rw [← smul_eval_smul, smul_inv_smul]
 
@@ -80,7 +81,7 @@ open mul_action
 open_locale classical
 
 /-- the product of `(X - g • x)` over distinct `g • x`. -/
-noncomputable def prod_X_sub_smul (x : R) : polynomial R :=
+noncomputable def prod_X_sub_smul (x : R) : R[X] :=
 (finset.univ : finset (G ⧸ mul_action.stabilizer G x)).prod $
 λ g, polynomial.X - polynomial.C (of_quotient_stabilizer G x g)
 
@@ -89,7 +90,7 @@ polynomial.monic_prod_of_monic _ _ $ λ g _, polynomial.monic_X_sub_C _
 
 theorem prod_X_sub_smul.eval (x : R) : (prod_X_sub_smul G R x).eval x = 0 :=
 (monoid_hom.map_prod
-  ((polynomial.aeval x).to_ring_hom.to_monoid_hom : polynomial R →* R) _ _).trans $
+  ((polynomial.aeval x).to_ring_hom.to_monoid_hom : R[X] →* R) _ _).trans $
   finset.prod_eq_zero (finset.mem_univ $ quotient_group.mk 1) $
   by simp
 
@@ -112,7 +113,7 @@ variables {Q : Type*} [comm_semiring Q] [mul_semiring_action M Q]
 open polynomial
 
 /-- An equivariant map induces an equivariant map on polynomials. -/
-protected noncomputable def polynomial (g : P →+*[M] Q) : polynomial P →+*[M] polynomial Q :=
+protected noncomputable def polynomial (g : P →+*[M] Q) : P[X] →+*[M] Q[X] :=
 { to_fun := map g,
   map_smul' := λ m p, polynomial.induction_on p
     (λ b, by rw [smul_C, map_C, coe_fn_coe, g.map_smul, map_C, coe_fn_coe, smul_C])
@@ -126,7 +127,7 @@ protected noncomputable def polynomial (g : P →+*[M] Q) : polynomial P →+*[M
   map_mul' := λ p q, polynomial.map_mul g }
 
 @[simp] theorem coe_polynomial (g : P →+*[M] Q) :
-  (g.polynomial : polynomial P → polynomial Q) = map g :=
+  (g.polynomial : P[X] → Q[X]) = map g :=
 rfl
 
 end mul_semiring_action_hom

src/algebraic_geometry/prime_spectrum/is_open_comap_C.lean

@@ -14,12 +14,13 @@ https://stacks.math.columbia.edu/tag/00FB
 -/
 
 open ideal polynomial prime_spectrum set
+open_locale polynomial
 
 namespace algebraic_geometry
 
 namespace polynomial
 
-variables {R : Type*} [comm_ring R] {f : polynomial R}
+variables {R : Type*} [comm_ring R] {f : R[X]}
 
 /-- Given a polynomial `f ∈ R[x]`, `image_of_Df` is the subset of `Spec R` where at least one
 of the coefficients of `f` does not vanish.  Lemma `image_of_Df_eq_comap_C_compl_zero_locus`
@@ -37,15 +38,15 @@ end
 /-- If a point of `Spec R[x]` is not contained in the vanishing set of `f`, then its image in
 `Spec R` is contained in the open set where at least one of the coefficients of `f` is non-zero.
 This lemma is a reformulation of `exists_coeff_not_mem_C_inverse`. -/
-lemma comap_C_mem_image_of_Df {I : prime_spectrum (polynomial R)}
-  (H : I ∈ (zero_locus {f} : set (prime_spectrum (polynomial R)))ᶜ ) :
-  prime_spectrum.comap (polynomial.C : R →+* polynomial R) I ∈ image_of_Df f :=
+lemma comap_C_mem_image_of_Df {I : prime_spectrum R[X]}
+  (H : I ∈ (zero_locus {f} : set (prime_spectrum R[X]))ᶜ ) :
+  prime_spectrum.comap (polynomial.C : R →+* R[X]) I ∈ image_of_Df f :=
 exists_coeff_not_mem_C_inverse (mem_compl_zero_locus_iff_not_mem.mp H)
 
 /-- The open set `image_of_Df f` coincides with the image of `basic_open f` under the
 morphism `C⁺ : Spec R[x] → Spec R`. -/
 lemma image_of_Df_eq_comap_C_compl_zero_locus :
-  image_of_Df f = prime_spectrum.comap (C : R →+* polynomial R) '' (zero_locus {f})ᶜ :=
+  image_of_Df f = prime_spectrum.comap (C : R →+* R[X]) '' (zero_locus {f})ᶜ :=
 begin
   refine ext (λ x, ⟨λ hx, ⟨⟨map C x.val, (is_prime_map_C_of_is_prime x.property)⟩, ⟨_, _⟩⟩, _⟩),
   { rw [mem_compl_eq, mem_zero_locus, singleton_subset_iff],
@@ -64,7 +65,7 @@ Stacks Project "Lemma 00FB", first part.
 https://stacks.math.columbia.edu/tag/00FB
 -/
 theorem is_open_map_comap_C :
-  is_open_map (prime_spectrum.comap (C : R →+* polynomial R)) :=
+  is_open_map (prime_spectrum.comap (C : R →+* R[X])) :=
 begin
   rintros U ⟨s, z⟩,
   rw [← compl_compl U, ← z, ← Union_of_singleton_coe s, zero_locus_Union, compl_Inter, image_Union],

src/analysis/calculus/deriv.lean

@@ -83,7 +83,7 @@ See the explanations there.
 
 universes u v w
 noncomputable theory
-open_locale classical topological_space big_operators filter ennreal
+open_locale classical topological_space big_operators filter ennreal polynomial
 open filter asymptotics set
 open continuous_linear_map (smul_right smul_right_one_eq_iff)
 
@@ -1774,7 +1774,7 @@ namespace polynomial
 /-! ### Derivative of a polynomial -/
 
 variables {x : 𝕜} {s : set 𝕜}
-variable (p : polynomial 𝕜)
+variable (p : 𝕜[X])
 
 /-- The derivative (in the analysis sense) of a polynomial `p` is given by `p.derivative`. -/
 protected lemma has_strict_deriv_at (x : 𝕜) :

src/analysis/calculus/local_extr.lean

@@ -65,7 +65,7 @@ local extremum, Fermat's Theorem, Rolle's Theorem
 universes u v
 
 open filter set
-open_locale topological_space classical
+open_locale topological_space classical polynomial
 
 section module
 
@@ -357,7 +357,7 @@ end Rolle
 
 namespace polynomial
 
-lemma card_root_set_le_derivative {F : Type*} [field F] [algebra F ℝ] (p : polynomial F) :
+lemma card_root_set_le_derivative {F : Type*} [field F] [algebra F ℝ] (p : F[X]) :
   fintype.card (p.root_set ℝ) ≤ fintype.card (p.derivative.root_set ℝ) + 1 :=
 begin
   haveI : char_zero F :=