bump to nightly-2023-03-08-10

mathlib commit leanprover-community/mathlib3@38f16f9

Mathbin/Algebra/Algebra/Spectrum.lean

@@ -341,7 +341,7 @@ theorem sub_singleton_eq (a : A) (r : R) : σ a - {r} = σ (a - ↑ₐ r) := by
 open Polynomial
 
 theorem exists_mem_of_not_isUnit_aeval_prod [IsDomain R] {p : R[X]} {a : A} (hp : p ≠ 0)
-    (h : ¬IsUnit (aeval a (Multiset.map (fun x : R => x - c x) p.roots).Prod)) :
+    (h : ¬IsUnit (aeval a (Multiset.map (fun x : R => X - C x) p.roots).Prod)) :
     ∃ k : R, k ∈ σ a ∧ eval k p = 0 :=
   by
   rw [← Multiset.prod_toList, AlgHom.map_list_prod] at h

Mathbin/Algebra/CubicDiscriminant.lean

@@ -64,19 +64,19 @@ variable {P Q : Cubic R} {a b c d a' b' c' d' : R} [Semiring R]
 
 /-- Convert a cubic polynomial to a polynomial. -/
 def toPoly (P : Cubic R) : R[X] :=
-  c P.a * x ^ 3 + c P.b * x ^ 2 + c P.c * x + c P.d
+  C P.a * X ^ 3 + C P.b * X ^ 2 + C P.c * X + C P.d
 #align cubic.to_poly Cubic.toPoly
 
 theorem c_mul_prod_x_sub_c_eq [CommRing S] {w x y z : S} :
-    c w * (x - c x) * (x - c y) * (x - c z) =
+    C w * (X - C x) * (X - C y) * (X - C z) =
       toPoly ⟨w, w * -(x + y + z), w * (x * y + x * z + y * z), w * -(x * y * z)⟩ :=
   by
   simp only [to_poly, C_neg, C_add, C_mul]
   ring1
 #align cubic.C_mul_prod_X_sub_C_eq Cubic.c_mul_prod_x_sub_c_eq
 
 theorem prod_x_sub_c_eq [CommRing S] {x y z : S} :
-    (x - c x) * (x - c y) * (x - c z) =
+    (X - C x) * (X - C y) * (X - C z) =
       toPoly ⟨1, -(x + y + z), x * y + x * z + y * z, -(x * y * z)⟩ :=
   by rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]
 #align cubic.prod_X_sub_C_eq Cubic.prod_x_sub_c_eq
@@ -140,27 +140,27 @@ theorem toPoly_injective (P Q : Cubic R) : P.toPoly = Q.toPoly ↔ P = Q :=
   ⟨fun h => ext P Q (a_of_eq h) (b_of_eq h) (c_of_eq h) (d_of_eq h), congr_arg toPoly⟩
 #align cubic.to_poly_injective Cubic.toPoly_injective
 
-theorem of_a_eq_zero (ha : P.a = 0) : P.toPoly = c P.b * x ^ 2 + c P.c * x + c P.d := by
+theorem of_a_eq_zero (ha : P.a = 0) : P.toPoly = C P.b * X ^ 2 + C P.c * X + C P.d := by
   rw [to_poly, ha, C_0, zero_mul, zero_add]
 #align cubic.of_a_eq_zero Cubic.of_a_eq_zero
 
-theorem of_a_eq_zero' : toPoly ⟨0, b, c, d⟩ = c b * x ^ 2 + c c * x + c d :=
+theorem of_a_eq_zero' : toPoly ⟨0, b, c, d⟩ = C b * X ^ 2 + C c * X + C d :=
   of_a_eq_zero rfl
 #align cubic.of_a_eq_zero' Cubic.of_a_eq_zero'
 
-theorem of_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.toPoly = c P.c * x + c P.d := by
+theorem of_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.toPoly = C P.c * X + C P.d := by
   rw [of_a_eq_zero ha, hb, C_0, zero_mul, zero_add]
 #align cubic.of_b_eq_zero Cubic.of_b_eq_zero
 
-theorem of_b_eq_zero' : toPoly ⟨0, 0, c, d⟩ = c c * x + c d :=
+theorem of_b_eq_zero' : toPoly ⟨0, 0, c, d⟩ = C c * X + C d :=
   of_b_eq_zero rfl rfl
 #align cubic.of_b_eq_zero' Cubic.of_b_eq_zero'
 
-theorem of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.toPoly = c P.d := by
+theorem of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.toPoly = C P.d := by
   rw [of_b_eq_zero ha hb, hc, C_0, zero_mul, zero_add]
 #align cubic.of_c_eq_zero Cubic.of_c_eq_zero
 
-theorem of_c_eq_zero' : toPoly ⟨0, 0, 0, d⟩ = c d :=
+theorem of_c_eq_zero' : toPoly ⟨0, 0, 0, d⟩ = C d :=
   of_c_eq_zero rfl rfl rfl
 #align cubic.of_c_eq_zero' Cubic.of_c_eq_zero'
 
@@ -538,7 +538,7 @@ theorem splits_iff_roots_eq_three (ha : P.a ≠ 0) :
 #align cubic.splits_iff_roots_eq_three Cubic.splits_iff_roots_eq_three
 
 theorem eq_prod_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
-    (map φ P).toPoly = c (φ P.a) * (x - c x) * (x - c y) * (x - c z) :=
+    (map φ P).toPoly = C (φ P.a) * (X - C x) * (X - C y) * (X - C z) :=
   by
   rw [map_to_poly,
     eq_prod_roots_of_splits <|

Mathbin/Algebra/DirectLimit.lean

@@ -433,7 +433,7 @@ theorem Polynomial.exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)]
   Polynomial.induction_on q
     (fun z =>
       let ⟨i, x, h⟩ := exists_of z
-      ⟨i, c x, by rw [map_C, h]⟩)
+      ⟨i, C x, by rw [map_C, h]⟩)
     (fun q₁ q₂ ⟨i₁, p₁, ih₁⟩ ⟨i₂, p₂, ih₂⟩ =>
       let ⟨i, h1, h2⟩ := exists_ge_ge i₁ i₂
       ⟨i, p₁.map (f' i₁ i h1) + p₂.map (f' i₂ i h2),
@@ -442,7 +442,7 @@ theorem Polynomial.exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)]
         congr 2 <;> ext x <;> simp_rw [RingHom.comp_apply, of_f]⟩)
     fun n z ih =>
     let ⟨i, x, h⟩ := exists_of z
-    ⟨i, c x * x ^ (n + 1), by rw [Polynomial.map_mul, map_C, h, Polynomial.map_pow, map_X]⟩
+    ⟨i, C x * X ^ (n + 1), by rw [Polynomial.map_mul, map_C, h, Polynomial.map_pow, map_X]⟩
 #align ring.direct_limit.polynomial.exists_of Ring.DirectLimit.Polynomial.exists_of
 
 end

Mathbin/Algebra/Polynomial/BigOperators.lean

@@ -258,7 +258,7 @@ open Monic
 -- Eventually this can be generalized with Vieta's formulas
 -- plus the connection between roots and factorization.
 theorem multiset_prod_x_sub_c_nextCoeff (t : Multiset R) :
-    nextCoeff (t.map fun x => x - c x).Prod = -t.Sum :=
+    nextCoeff (t.map fun x => X - C x).Prod = -t.Sum :=
   by
   rw [next_coeff_multiset_prod]
   · simp only [next_coeff_X_sub_C]
@@ -268,12 +268,12 @@ theorem multiset_prod_x_sub_c_nextCoeff (t : Multiset R) :
 #align polynomial.multiset_prod_X_sub_C_next_coeff Polynomial.multiset_prod_x_sub_c_nextCoeff
 
 theorem prod_x_sub_c_nextCoeff {s : Finset ι} (f : ι → R) :
-    nextCoeff (∏ i in s, x - c (f i)) = -∑ i in s, f i := by
+    nextCoeff (∏ i in s, X - C (f i)) = -∑ i in s, f i := by
   simpa using multiset_prod_X_sub_C_next_coeff (s.1.map f)
 #align polynomial.prod_X_sub_C_next_coeff Polynomial.prod_x_sub_c_nextCoeff
 
 theorem multiset_prod_x_sub_c_coeff_card_pred (t : Multiset R) (ht : 0 < t.card) :
-    (t.map fun x => x - c x).Prod.coeff (t.card - 1) = -t.Sum :=
+    (t.map fun x => X - C x).Prod.coeff (t.card - 1) = -t.Sum :=
   by
   nontriviality R
   convert multiset_prod_X_sub_C_next_coeff (by assumption)
@@ -290,7 +290,7 @@ theorem multiset_prod_x_sub_c_coeff_card_pred (t : Multiset R) (ht : 0 < t.card)
 #align polynomial.multiset_prod_X_sub_C_coeff_card_pred Polynomial.multiset_prod_x_sub_c_coeff_card_pred
 
 theorem prod_x_sub_c_coeff_card_pred (s : Finset ι) (f : ι → R) (hs : 0 < s.card) :
-    (∏ i in s, x - c (f i)).coeff (s.card - 1) = -∑ i in s, f i := by
+    (∏ i in s, X - C (f i)).coeff (s.card - 1) = -∑ i in s, f i := by
   simpa using multiset_prod_X_sub_C_coeff_card_pred (s.1.map f) (by simpa using hs)
 #align polynomial.prod_X_sub_C_coeff_card_pred Polynomial.prod_x_sub_c_coeff_card_pred
 

Mathbin/Algebra/Polynomial/GroupRingAction.lean

@@ -60,7 +60,7 @@ variable {M R}
 variable [MulSemiringAction M R]
 
 @[simp]
-theorem smul_x (m : M) : (m • x : R[X]) = x :=
+theorem smul_x (m : M) : (m • X : R[X]) = X :=
   (smul_eq_map R m).symm ▸ map_x _
 #align polynomial.smul_X Polynomial.smul_x
 
@@ -98,7 +98,7 @@ open Classical
 /-- the product of `(X - g • x)` over distinct `g • x`. -/
 noncomputable def prodXSubSmul (x : R) : R[X] :=
   (Finset.univ : Finset (G ⧸ MulAction.stabilizer G x)).Prod fun g =>
-    Polynomial.x - Polynomial.c (ofQuotientStabilizer G x g)
+    Polynomial.X - Polynomial.C (ofQuotientStabilizer G x g)
 #align prod_X_sub_smul prodXSubSmul
 
 theorem prodXSubSmul.monic (x : R) : (prodXSubSmul G R x).Monic :=
@@ -113,7 +113,7 @@ theorem prodXSubSmul.eval (x : R) : (prodXSubSmul G R x).eval x = 0 :=
 theorem prodXSubSmul.smul (x : R) (g : G) : g • prodXSubSmul G R x = prodXSubSmul G R x :=
   Finset.smul_prod.trans <|
     Fintype.prod_bijective _ (MulAction.bijective g) _ _ fun g' => by
-      rw [of_quotient_stabilizer_smul, smul_sub, Polynomial.smul_x, Polynomial.smul_c]
+      rw [of_quotient_stabilizer_smul, smul_sub, Polynomial.smul_x, Polynomial.smul_C]
 #align prod_X_sub_smul.smul prodXSubSmul.smul
 
 theorem prodXSubSmul.coeff (x : R) (g : G) (n : ℕ) :

Mathbin/AlgebraicGeometry/EllipticCurve/Point.lean

@@ -112,7 +112,7 @@ variable {R : Type u} [CommRing R] (W : WeierstrassCurve R) (A : Type v) [CommRi
 
 /-- The polynomial $-Y - a_1X - a_3$ associated to negation. -/
 noncomputable def negPolynomial : R[X][Y] :=
-  -Y - c (c W.a₁ * x + c W.a₃)
+  -Y - C (C W.a₁ * X + C W.a₃)
 #align weierstrass_curve.neg_polynomial WeierstrassCurve.negPolynomial
 
 /-- The $Y$-coordinate of the negation of an affine point in `W`.
@@ -148,7 +148,7 @@ theorem baseChange_negY_of_baseChange (x₁ y₁ : A) :
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.1038319287.eval_simp -/
 @[simp]
-theorem eval_negPolynomial : (W.negPolynomial.eval <| c y₁).eval x₁ = W.negY x₁ y₁ :=
+theorem eval_negPolynomial : (W.negPolynomial.eval <| C y₁).eval x₁ = W.negY x₁ y₁ :=
   by
   rw [neg_Y, sub_sub, neg_polynomial]
   run_tac
@@ -160,7 +160,7 @@ with a slope of $L$ that passes through an affine point $(x_1, y_1)$.
 
 This does not depend on `W`, and has argument order: $x_1$, $y_1$, $L$. -/
 noncomputable def linePolynomial : R[X] :=
-  c L * (x - c x₁) + c y₁
+  C L * (X - C x₁) + C y₁
 #align weierstrass_curve.line_polynomial WeierstrassCurve.linePolynomial
 
 /-- The polynomial obtained by substituting the line $Y = L(X - x_1) + y_1$, with a slope of $L$
@@ -451,7 +451,7 @@ theorem slope_of_X_ne (hx : x₁ ≠ x₂) : W.slope x₁ x₂ y₁ y₂ = (y₁
 
 theorem slope_of_Y_ne_eq_eval (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) :
     W.slope x₁ x₂ y₁ y₂ =
-      -(W.polynomialX.eval <| c y₁).eval x₁ / (W.polynomialY.eval <| c y₁).eval x₁ :=
+      -(W.polynomialX.eval <| C y₁).eval x₁ / (W.polynomialY.eval <| C y₁).eval x₁ :=
   by
   rw [slope_of_Y_ne hx hy, eval_polynomial_X, neg_sub]
   congr 1
@@ -509,7 +509,7 @@ theorem Y_eq_of_Y_ne (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) : y₁
 
 theorem addPolynomial_slope (hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) :
     W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) =
-      -((x - c x₁) * (x - c x₂) * (x - c (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂))) :=
+      -((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂))) :=
   by
   rw [add_polynomial_eq, neg_inj, Cubic.prod_x_sub_c_eq, Cubic.toPoly_injective]
   by_cases hx : x₁ = x₂
@@ -540,8 +540,8 @@ theorem addPolynomial_slope (hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) :
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.150691367.derivative_simp -/
 theorem derivative_addPolynomial_slope (hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂) :
     derivative (W.addPolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) =
-      -((x - c x₁) * (x - c x₂) + (x - c x₁) * (x - c (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂)) +
-          (x - c x₂) * (x - c (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂))) :=
+      -((X - C x₁) * (X - C x₂) + (X - C x₁) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂)) +
+          (X - C x₂) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂))) :=
   by
   rw [add_polynomial_slope h₁' h₂' hxy]
   run_tac

Mathbin/AlgebraicGeometry/EllipticCurve/Weierstrass.lean

@@ -376,7 +376,7 @@ theorem twoTorsionPolynomial_disc_ne_zero [Nontrivial R] [Invertible (2 : R)] (h
 end TorsionPolynomial
 
 -- mathport name: outer_variable
-scoped[PolynomialPolynomial] notation "Y" => Polynomial.x
+scoped[PolynomialPolynomial] notation "Y" => Polynomial.X
 
 -- mathport name: polynomial_polynomial
 scoped[PolynomialPolynomial] notation R "[X][Y]" => Polynomial (Polynomial R)
@@ -396,7 +396,7 @@ of type `R[X][X]`, where the inner variable represents $X$ and the outer variabl
 For clarity, the alternative notations `Y` and `R[X][Y]` are provided in the `polynomial_polynomial`
 locale to represent the outer variable and the bivariate polynomial ring `R[X][X]` respectively. -/
 protected noncomputable def polynomial : R[X][Y] :=
-  Y ^ 2 + c (c W.a₁ * x + c W.a₃) * Y - c (x ^ 3 + c W.a₂ * x ^ 2 + c W.a₄ * x + c W.a₆)
+  Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)
 #align weierstrass_curve.polynomial WeierstrassCurve.polynomial
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.3266784253.C_simp -/
@@ -455,7 +455,7 @@ theorem irreducible_polynomial [IsDomain R] : Irreducible W.Polynomial :=
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.3143603269.eval_simp -/
 @[simp]
 theorem eval_polynomial (x y : R) :
-    (W.Polynomial.eval <| c y).eval x =
+    (W.Polynomial.eval <| C y).eval x =
       y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) :=
   by
   simp only [WeierstrassCurve.polynomial]
@@ -471,7 +471,7 @@ theorem eval_polynomial_zero : (W.Polynomial.eval 0).eval 0 = -W.a₆ := by
 
 /-- The proposition that an affine point $(x, y)$ lies in `W`. In other words, $W(x, y) = 0$. -/
 def Equation (x y : R) : Prop :=
-  (W.Polynomial.eval <| c y).eval x = 0
+  (W.Polynomial.eval <| C y).eval x = 0
 #align weierstrass_curve.equation WeierstrassCurve.Equation
 
 theorem equation_iff' (x y : R) :
@@ -530,13 +530,13 @@ theorem equation_iff_baseChange_of_baseChange [Nontrivial B] [NoZeroSMulDivisors
 
 TODO: define this in terms of `polynomial.derivative`. -/
 noncomputable def polynomialX : R[X][Y] :=
-  c (c W.a₁) * Y - c (c 3 * x ^ 2 + c (2 * W.a₂) * x + c W.a₄)
+  C (C W.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W.a₂) * X + C W.a₄)
 #align weierstrass_curve.polynomial_X WeierstrassCurve.polynomialX
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.3143603269.eval_simp -/
 @[simp]
 theorem eval_polynomialX (x y : R) :
-    (W.polynomialX.eval <| c y).eval x = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) :=
+    (W.polynomialX.eval <| C y).eval x = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) :=
   by
   simp only [polynomial_X]
   run_tac
@@ -552,12 +552,12 @@ theorem eval_polynomialX_zero : (W.polynomialX.eval 0).eval 0 = -W.a₄ := by
 
 TODO: define this in terms of `polynomial.derivative`. -/
 noncomputable def polynomialY : R[X][Y] :=
-  c (c 2) * Y + c (c W.a₁ * x + c W.a₃)
+  C (C 2) * Y + C (C W.a₁ * X + C W.a₃)
 #align weierstrass_curve.polynomial_Y WeierstrassCurve.polynomialY
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.3143603269.eval_simp -/
 @[simp]
-theorem eval_polynomialY (x y : R) : (W.polynomialY.eval <| c y).eval x = 2 * y + W.a₁ * x + W.a₃ :=
+theorem eval_polynomialY (x y : R) : (W.polynomialY.eval <| C y).eval x = 2 * y + W.a₁ * x + W.a₃ :=
   by
   simp only [polynomial_Y]
   run_tac
@@ -573,7 +573,7 @@ theorem eval_polynomialY_zero : (W.polynomialY.eval 0).eval 0 = W.a₃ := by
 /-- The proposition that an affine point $(x, y)$ on `W` is nonsingular.
 In other words, either $W_X(x, y) \ne 0$ or $W_Y(x, y) \ne 0$. -/
 def Nonsingular (x y : R) : Prop :=
-  W.Equation x y ∧ ((W.polynomialX.eval <| c y).eval x ≠ 0 ∨ (W.polynomialY.eval <| c y).eval x ≠ 0)
+  W.Equation x y ∧ ((W.polynomialX.eval <| C y).eval x ≠ 0 ∨ (W.polynomialY.eval <| C y).eval x ≠ 0)
 #align weierstrass_curve.nonsingular WeierstrassCurve.Nonsingular
 
 theorem nonsingular_iff' (x y : R) :
@@ -686,11 +686,11 @@ variable (x : R) (y : R[X])
 /-- The class of the element $X - x$ in $R[W]$ for some $x \in R$. -/
 @[simp]
 noncomputable def xClass : W.CoordinateRing :=
-  AdjoinRoot.mk W.Polynomial <| c <| x - c x
+  AdjoinRoot.mk W.Polynomial <| C <| X - C x
 #align weierstrass_curve.coordinate_ring.X_class WeierstrassCurve.CoordinateRing.xClass
 
 theorem xClass_ne_zero [Nontrivial R] : xClass W x ≠ 0 :=
-  AdjoinRoot.mk_ne_zero_of_natDegree_lt W.monic_polynomial (c_ne_zero.mpr <| x_sub_c_ne_zero x) <|
+  AdjoinRoot.mk_ne_zero_of_natDegree_lt W.monic_polynomial (C_ne_zero.mpr <| x_sub_c_ne_zero x) <|
     by
     rw [nat_degree_polynomial, nat_degree_C]
     norm_num1
@@ -699,7 +699,7 @@ theorem xClass_ne_zero [Nontrivial R] : xClass W x ≠ 0 :=
 /-- The class of the element $Y - y(X)$ in $R[W]$ for some $y(X) \in R[X]$. -/
 @[simp]
 noncomputable def yClass : W.CoordinateRing :=
-  AdjoinRoot.mk W.Polynomial <| Y - c y
+  AdjoinRoot.mk W.Polynomial <| Y - C y
 #align weierstrass_curve.coordinate_ring.Y_class WeierstrassCurve.CoordinateRing.yClass
 
 theorem yClass_ne_zero [Nontrivial R] : yClass W y ≠ 0 :=
@@ -771,7 +771,7 @@ theorem coe_basis :
 
 variable {W}
 
-theorem smul (x : R[X]) (y : W.CoordinateRing) : x • y = AdjoinRoot.mk W.Polynomial (c x) * y :=
+theorem smul (x : R[X]) (y : W.CoordinateRing) : x • y = AdjoinRoot.mk W.Polynomial (C x) * y :=
   (algebraMap_smul W.CoordinateRing x y).symm
 #align weierstrass_curve.coordinate_ring.smul WeierstrassCurve.CoordinateRing.smul
 
@@ -794,7 +794,7 @@ theorem exists_smul_basis_eq (x : W.CoordinateRing) :
 variable (W)
 
 theorem smul_basis_mul_c (p q : R[X]) :
-    (p • 1 + q • AdjoinRoot.mk W.Polynomial Y) * AdjoinRoot.mk W.Polynomial (c y) =
+    (p • 1 + q • AdjoinRoot.mk W.Polynomial Y) * AdjoinRoot.mk W.Polynomial (C y) =
       (p * y) • 1 + (q * y) • AdjoinRoot.mk W.Polynomial Y :=
   by
   simp only [smul, map_mul]
@@ -803,8 +803,8 @@ theorem smul_basis_mul_c (p q : R[X]) :
 
 theorem smul_basis_mul_Y (p q : R[X]) :
     (p • 1 + q • AdjoinRoot.mk W.Polynomial Y) * AdjoinRoot.mk W.Polynomial Y =
-      (q * (x ^ 3 + c W.a₂ * x ^ 2 + c W.a₄ * x + c W.a₆)) • 1 +
-        (p - q * (c W.a₁ * x + c W.a₃)) • AdjoinRoot.mk W.Polynomial Y :=
+      (q * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) • 1 +
+        (p - q * (C W.a₁ * X + C W.a₃)) • AdjoinRoot.mk W.Polynomial Y :=
   by
   have Y_sq :
     AdjoinRoot.mk W.polynomial Y ^ 2 =
@@ -823,8 +823,8 @@ theorem smul_basis_mul_Y (p q : R[X]) :
 
 theorem norm_smul_basis (p q : R[X]) :
     Algebra.norm R[X] (p • 1 + q • AdjoinRoot.mk W.Polynomial Y) =
-      p ^ 2 - p * q * (c W.a₁ * x + c W.a₃) -
-        q ^ 2 * (x ^ 3 + c W.a₂ * x ^ 2 + c W.a₄ * x + c W.a₆) :=
+      p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) -
+        q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) :=
   by
   simp_rw [Algebra.norm_eq_matrix_det W.CoordinateRing.Basis, Matrix.det_fin_two,
     Algebra.leftMulMatrix_eq_repr_mul, basis_zero, mul_one, basis_one, smul_basis_mul_Y, map_add,
@@ -836,9 +836,9 @@ theorem norm_smul_basis (p q : R[X]) :
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic _private.3266784253.C_simp -/
 theorem coe_norm_smul_basis (p q : R[X]) :
     ↑(Algebra.norm R[X] <| p • 1 + q • AdjoinRoot.mk W.Polynomial Y) =
-      AdjoinRoot.mk W.Polynomial ((c p + c q * x) * (c p + c q * (-x - c (c W.a₁ * x + c W.a₃)))) :=
+      AdjoinRoot.mk W.Polynomial ((C p + C q * X) * (C p + C q * (-X - C (C W.a₁ * X + C W.a₃)))) :=
   AdjoinRoot.mk_eq_mk.mpr
-    ⟨c q ^ 2, by
+    ⟨C q ^ 2, by
       rw [norm_smul_basis, WeierstrassCurve.polynomial]
       run_tac
         C_simp