[Merged by Bors] - refactor(data/polynomial): use linear_map for monomial, review degree

src/algebra/algebra/basic.lean

@@ -521,7 +521,7 @@ end comm_semiring
 
 section ring
 
-variables [comm_ring R] [ring A] [ring B]
+variables [comm_semiring R] [ring A] [ring B]
 variables [algebra R A] [algebra R B] (φ : A →ₐ[R] B)
 
 @[simp] lemma map_neg (x) : φ (-x) = -φ x :=
@@ -530,6 +530,9 @@ variables [algebra R A] [algebra R B] (φ : A →ₐ[R] B)
 @[simp] lemma map_sub (x y) : φ (x - y) = φ x - φ y :=
 φ.to_ring_hom.map_sub x y
 
+@[simp] lemma map_int_cast (n : ℤ) : φ n = n :=
+φ.to_ring_hom.map_int_cast n
+
 end ring
 
 section division_ring

src/algebra/group/basic.lean

@@ -169,6 +169,10 @@ by have := @mul_right_inj _ _ a a 1; rwa mul_one at this
 theorem inv_eq_one : a⁻¹ = 1 ↔ a = 1 :=
 by rw [← @inv_inj _ _ a 1, one_inv]
 
+@[simp, to_additive]
+theorem one_eq_inv : 1 = a⁻¹ ↔ a = 1 :=
+by rw [eq_comm, inv_eq_one]
+
 @[to_additive]
 theorem inv_ne_one : a⁻¹ ≠ 1 ↔ a ≠ 1 :=
 not_congr inv_eq_one

src/analysis/calculus/deriv.lean

@@ -1532,7 +1532,7 @@ lemma has_strict_deriv_at_pow (n : ℕ) (x : 𝕜) :
 begin
   convert (polynomial.C (1 : 𝕜) * (polynomial.X)^n).has_strict_deriv_at x,
   { simp },
-  { rw [polynomial.derivative_monomial], simp }
+  { rw [polynomial.derivative_C_mul_X_pow], simp }
 end
 
 lemma has_deriv_at_pow (n : ℕ) (x : 𝕜) : has_deriv_at (λx, x^n) ((n : 𝕜) * x^(n-1)) x :=

src/data/polynomial/algebra_map.lean

@@ -79,9 +79,8 @@ eval₂_algebra_map_X p { commutes' := λ n, by simp, .. f }
 section comp
 
 lemma eval₂_comp [comm_semiring S] (f : R →+* S) {x : S} :
-  (p.comp q).eval₂ f x = p.eval₂ f (q.eval₂ f x) :=
-by rw [comp, p.as_sum_range]; simp only [eval₂_mul, eval₂_C, eval₂_pow, eval₂_finset_sum, eval₂_X]
-
+  eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q) p :=
+by rw [comp, p.as_sum_range]; simp [eval₂_finset_sum, eval₂_pow]
 
 lemma eval_comp : (p.comp q).eval a = p.eval (q.eval a) := eval₂_comp _
 

src/data/polynomial/basic.lean

@@ -35,20 +35,22 @@ variables [semiring R] {p q : polynomial R}
 
 instance : inhabited (polynomial R) := add_monoid_algebra.inhabited _ _
 instance : semiring (polynomial R) := add_monoid_algebra.semiring
-instance : has_scalar R (polynomial R) := add_monoid_algebra.has_scalar
-instance : semimodule R (polynomial R) := add_monoid_algebra.semimodule
+instance {S} [semiring S] [semimodule S R] : semimodule S (polynomial R) :=
+add_monoid_algebra.semimodule
 
 instance [subsingleton R] : unique (polynomial R) := add_monoid_algebra.unique
 
 @[simp] lemma support_zero : (0 : polynomial R).support = ∅ := rfl
 
 /-- `monomial s a` is the monomial `a * X^s` -/
-def monomial (n : ℕ) (a : R) : polynomial R := finsupp.single n a
+def monomial (n : ℕ) : R →ₗ[R] polynomial R := finsupp.lsingle n
 
-@[simp] lemma monomial_zero_right (n : ℕ) :
+lemma monomial_zero_right (n : ℕ) :
   monomial n (0 : R) = 0 :=
 finsupp.single_zero
 
+lemma monomial_def (n : ℕ) (a : R) : monomial n a = finsupp.single n a := rfl
+
 lemma monomial_add (n : ℕ) (r s : R) :
   monomial n (r + s) = monomial n r + monomial n s :=
 finsupp.single_add
@@ -57,6 +59,9 @@ lemma monomial_mul_monomial (n m : ℕ) (r s : R) :
   monomial n r * monomial m s = monomial (n + m) (r * s) :=
 add_monoid_algebra.single_mul_single
 
+lemma smul_monomial {S} [semiring S] [semimodule S R] (a : S) (n : ℕ) (b : R) :
+  a • monomial n b = monomial n (a • b) :=
+finsupp.smul_single _ _ _
 
 /-- `X` is the polynomial variable (aka indeterminant). -/
 def X : polynomial R := monomial 1 1
@@ -116,8 +121,7 @@ lemma X_pow_eq_monomial (n) : X ^ n = monomial n (1:R) :=
 begin
   induction n with n hn,
   { refl, },
-  { conv_rhs {rw nat.succ_eq_add_one, congr, skip, rw ← mul_one (1:R)},
-    rw [← monomial_mul_monomial, ← hn, pow_succ, X_mul, X], },
+  { rw [pow_succ', hn, X, monomial_mul_monomial, one_mul] },
 end
 
 lemma support_X_pow (H : ¬ (1:R) = 0) (n : ℕ) : (X^n : polynomial R).support = singleton n :=

src/data/polynomial/degree.lean

@@ -49,21 +49,9 @@ else with_bot.coe_le_coe.1 $
         (le_nat_degree_of_ne_zero (finsupp.mem_support_iff.1 hn))
         (nat.zero_le _))
 
-lemma eq_C_of_nat_degree_eq_zero (hp : p.nat_degree = 0) : p = C (p.coeff 0) :=
-begin
-  ext, induction n with n hn,
-  { simp only [polynomial.coeff_C_zero], },
-  { have ineq : p.nat_degree < n.succ := hp.symm ▸ n.succ_pos,
-    have zero1 : p.coeff n.succ = 0 := coeff_eq_zero_of_nat_degree_lt ineq,
-    have zero2 : (C (p.coeff 0)).nat_degree = 0 := nat_degree_C (p.coeff 0),
-    have zero3 : (C (p.coeff 0)).coeff n.succ = 0 :=
-      coeff_eq_zero_of_nat_degree_lt (zero2.symm ▸ n.succ_pos),
-    rw [zero1, zero3], }
-end
-
 lemma degree_map_le [semiring S] (f : R →+* S) :
-  degree (p.map f) ≤ degree p :=
-if h : p.map f = 0 then by simp [h]
+  degree (map f p) ≤ degree p :=
+if h : map f p = 0 then by simp [h]
 else begin
   rw [degree_eq_nat_degree h],
   refine le_degree_of_ne_zero (mt (congr_arg f) _),