feat(data/polynomial/*): more lemmas, especially for noncommutative rings (#6599)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebra/group_power/basic.lean

@@ -377,6 +377,13 @@ end comm_group
 lemma zero_pow [monoid_with_zero R] : ∀ {n : ℕ}, 0 < n → (0 : R) ^ n = 0
 | (n+1) _ := zero_mul _
 
+lemma zero_pow_eq [monoid_with_zero R] (n : ℕ) : (0 : R)^n = if n = 0 then 1 else 0 :=
+begin
+  split_ifs with h,
+  { rw [h, pow_zero], },
+  { rw [zero_pow (nat.pos_of_ne_zero h)] },
+end
+
 namespace ring_hom
 
 variables [semiring R] [semiring S]

src/algebra/monoid_algebra.lean

@@ -772,7 +772,6 @@ end derived_instances
 section misc_theorems
 
 variables [semiring k]
-local attribute [reducible] add_monoid_algebra
 
 lemma mul_apply [has_add G] (f g : add_monoid_algebra k G) (x : G) :
   (f * g) x = (f.sum $ λa₁ b₁, g.sum $ λa₂ b₂, if a₁ + a₂ = x then b₁ * b₂ else 0) :=
@@ -788,9 +787,18 @@ lemma support_mul [has_add G] (a b : add_monoid_algebra k G) :
 @monoid_algebra.support_mul k (multiplicative G) _ _ _ _
 
 lemma single_mul_single [has_add G] {a₁ a₂ : G} {b₁ b₂ : k} :
-  (single a₁ b₁ : add_monoid_algebra k G) * single a₂ b₂ = single (a₁ + a₂) (b₁ * b₂) :=
+  (single a₁ b₁ * single a₂ b₂ : add_monoid_algebra k G) = single (a₁ + a₂) (b₁ * b₂) :=
 @monoid_algebra.single_mul_single k (multiplicative G) _ _ _ _ _ _
 
+-- This should be a `@[simp]` lemma, but the simp_nf linter times out if we add this.
+-- Probably the correct fix is to make a `[add_]monoid_algebra.single` with the correct type,
+-- instead of relying on `finsupp.single`.
+lemma single_pow [add_monoid G] {a : G} {b : k} :
+  ∀ n : ℕ, ((single a b)^n : add_monoid_algebra k G) = single (n •ℕ a) (b ^ n)
+| 0 := rfl
+| (n+1) :=
+by rw [pow_succ, pow_succ, single_pow n, single_mul_single, add_comm, add_nsmul, one_nsmul]
+
 /-- Like `finsupp.map_domain_add`, but for the convolutive multiplication we define in this file -/
 lemma map_domain_mul {α : Type*} {β : Type*} {α₂ : Type*}
   [semiring β] [has_add α] [has_add α₂]
@@ -837,11 +845,11 @@ f.mul_single_apply_aux r _ _ _ $ λ a, by rw [add_zero]
 
 lemma single_mul_apply_aux [has_add G] (f : add_monoid_algebra k G) (r : k) (x y z : G)
   (H : ∀ a, x + a = y ↔ a = z) :
-  (single x r * f) y = r * f z :=
+  (single x r * f : add_monoid_algebra k G) y = r * f z :=
 @monoid_algebra.single_mul_apply_aux k (multiplicative G) _ _ _ _ _ _ _ H
 
 lemma single_zero_mul_apply [add_monoid G] (f : add_monoid_algebra k G) (r : k) (x : G) :
-  (single 0 r * f) x = r * f x :=
+  (single 0 r * f : add_monoid_algebra k G) x = r * f x :=
 f.single_mul_apply_aux r _ _ _ $ λ a, by rw [zero_add]
 
 lemma lift_nc_smul {R : Type*} [add_monoid G] [semiring R] (f : k →+* R)

src/data/int/cast.lean

@@ -109,6 +109,9 @@ def cast_ring_hom (α : Type*) [ring α] : ℤ →+* α := ⟨coe, cast_one, cas
 lemma cast_commute [ring α] (m : ℤ) (x : α) : commute ↑m x :=
 int.cases_on m (λ n, n.cast_commute x) (λ n, ((n+1).cast_commute x).neg_left)
 
+lemma cast_comm [ring α] (m : ℤ) (x : α) : (m : α) * x = x * m :=
+(cast_commute m x).eq
+
 lemma commute_cast [ring α] (x : α) (m : ℤ) : commute x m :=
 (m.cast_commute x).symm
 

src/data/nat/cast.lean

@@ -136,6 +136,9 @@ def cast_ring_hom (α : Type*) [semiring α] : ℕ →+* α :=
 lemma cast_commute [semiring α] (n : ℕ) (x : α) : commute ↑n x :=
 nat.rec_on n (commute.zero_left x) $ λ n ihn, ihn.add_left $ commute.one_left x
 
+lemma cast_comm [semiring α] (n : ℕ) (x : α) : (n : α) * x = x * n :=
+(cast_commute n x).eq
+
 lemma commute_cast [semiring α] (x : α) (n : ℕ) : commute x n :=
 (n.cast_commute x).symm
 

src/data/polynomial/algebra_map.lean

@@ -90,19 +90,6 @@ lemma eval₂_algebra_map_int_X {R : Type*} [ring R] (p : polynomial ℤ) (f : p
 -- Unfortunately `f.to_int_alg_hom` doesn't work here, as typeclasses don't match up correctly.
 eval₂_algebra_map_X p { commutes' := λ n, by simp, .. f }
 
-section comp
-
-lemma eval₂_comp [comm_semiring S] (f : R →+* S) {x : S} :
-  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 _
-
-instance comp.is_semiring_hom : is_semiring_hom (λ q : polynomial R, q.comp p) :=
-by unfold comp; apply_instance
-
-end comp
-
 end comm_semiring
 
 section aeval

src/data/polynomial/basic.lean

@@ -63,10 +63,14 @@ by simp
 /-- `monomial s a` is the monomial `a * X^s` -/
 def monomial (n : ℕ) : R →ₗ[R] polynomial R := finsupp.lsingle n
 
+@[simp]
 lemma monomial_zero_right (n : ℕ) :
   monomial n (0 : R) = 0 :=
 finsupp.single_zero
 
+-- This is not a `simp` lemma as `monomial_zero_left` is more general.
+lemma monomial_zero_one : monomial 0 (1 : R) = 1 := rfl
+
 lemma monomial_def (n : ℕ) (a : R) : monomial n a = finsupp.single n a := rfl
 
 lemma monomial_add (n : ℕ) (r s : R) :
@@ -77,6 +81,16 @@ 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
 
+@[simp]
+lemma monomial_pow (n : ℕ) (r : R) (k : ℕ) :
+  (monomial n r)^k = monomial (n*k) (r^k) :=
+begin
+  rw mul_comm,
+  convert add_monoid_algebra.single_pow k,
+  simp only [nat.cast_id, nsmul_eq_mul],
+  refl,
+end
+
 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 _ _ _
@@ -87,6 +101,14 @@ by convert @support_add _ _ _ p q
 /-- `X` is the polynomial variable (aka indeterminant). -/
 def X : polynomial R := monomial 1 1
 
+lemma monomial_one_one_eq_X : monomial 1 (1 : R) = X := rfl
+lemma monomial_one_right_eq_X_pow (n : ℕ) : monomial n 1 = X^n :=
+begin
+  induction n with n ih,
+  { simp [monomial_zero_one], },
+  { rw [pow_succ, ←ih, ←monomial_one_one_eq_X, monomial_mul_monomial, add_comm, one_mul], }
+end
+
 /-- `X` commutes with everything, even when the coefficients are noncommutative. -/
 lemma X_mul : X * p = p * X :=
 by { ext, simp [X, monomial, add_monoid_algebra.mul_apply, sum_single_index, add_comm] }
@@ -104,6 +126,26 @@ by rw [mul_assoc, X_pow_mul, ←mul_assoc]
 
 lemma commute_X (p : polynomial R) : commute X p := X_mul
 
+@[simp]
+lemma monomial_mul_X (n : ℕ) (r : R) : monomial n r * X = monomial (n+1) r :=
+by erw [monomial_mul_monomial, mul_one]
+
+@[simp]
+lemma monomial_mul_X_pow (n : ℕ) (r : R) (k : ℕ) : monomial n r * X^k = monomial (n+k) r :=
+begin
+  induction k with k ih,
+  { simp, },
+  { simp [ih, pow_succ', ←mul_assoc, add_assoc], },
+end
+
+@[simp]
+lemma X_mul_monomial (n : ℕ) (r : R) : X * monomial n r = monomial (n+1) r :=
+by rw [X_mul, monomial_mul_X]
+
+@[simp]
+lemma X_pow_mul_monomial (k n : ℕ) (r : R) : X^k * monomial n r = monomial (n+k) r :=
+by rw [X_pow_mul, monomial_mul_X_pow]
+
 /-- coeff p n is the coefficient of X^n in p -/
 def coeff (p : polynomial R) : ℕ → R := @coe_fn (ℕ →₀ R) _ p
 

src/data/polynomial/eval.lean

@@ -44,6 +44,17 @@ lemma eval₂_congr {R S : Type*} [semiring R] [semiring S]
   f = g → s = t → φ = ψ → eval₂ f s φ = eval₂ g t ψ :=
 by rintro rfl rfl rfl; refl
 
+@[simp] lemma eval₂_at_zero : p.eval₂ f 0 = f (coeff p 0) :=
+begin
+  -- This proof is lame, and the `finsupp` API shows through.
+  simp only [eval₂_eq_sum, zero_pow_eq, mul_ite, mul_zero, mul_one, finsupp.sum_ite_eq'],
+  split_ifs,
+  { refl, },
+  { simp only [not_not, finsupp.mem_support_iff, ne.def] at h,
+    apply_fun f at h,
+    simpa using h.symm, },
+end
+
 @[simp] lemma eval₂_zero : (0 : polynomial R).eval₂ f x = 0 :=
 finsupp.sum_zero_index
 
@@ -236,6 +247,26 @@ begin
   exact P.eval_eq_finset_sum x
 end
 
+@[simp] lemma eval₂_at_apply {S : Type*} [semiring S] (f : R →+* S) (r : R) :
+  p.eval₂ f (f r) = f (p.eval r) :=
+begin
+  rw [eval₂_eq_sum, eval_eq_sum, finsupp.sum, finsupp.sum, f.map_sum],
+  simp only [f.map_mul, f.map_pow],
+end
+
+@[simp] lemma eval₂_at_one {S : Type*} [semiring S] (f : R →+* S) : p.eval₂ f 1 = f (p.eval 1) :=
+begin
+  convert eval₂_at_apply f 1,
+  simp,
+end
+
+@[simp] lemma eval₂_at_nat_cast {S : Type*} [semiring S] (f : R →+* S) (n : ℕ) :
+  p.eval₂ f n = f (p.eval n) :=
+begin
+  convert eval₂_at_apply f n,
+  simp,
+end
+
 @[simp] lemma eval_C : (C a).eval x = a := eval₂_C _ _
 
 @[simp] lemma eval_nat_cast {n : ℕ} : (n : polynomial R).eval x = n :=
@@ -260,6 +291,35 @@ eval₂_monomial _ _
   (s • p).eval x = s * p.eval x :=
 eval₂_smul (ring_hom.id _) _ _
 
+@[simp] lemma eval_C_mul : (C a * p).eval x = a * p.eval x :=
+begin
+  apply polynomial.induction_on' p,
+  { intros p q ph qh,
+    simp only [mul_add, eval_add, ph, qh], },
+  { intros n b,
+    simp [mul_assoc], }
+end
+
+@[simp] lemma eval_nat_cast_mul {n : ℕ} : ((n : polynomial R) * p).eval x = n * p.eval x :=
+by rw [←C_eq_nat_cast, eval_C_mul]
+
+@[simp] lemma eval_mul_X : (p * X).eval x = p.eval x * x :=
+begin
+  apply polynomial.induction_on' p,
+  { intros p q ph qh,
+    simp only [add_mul, eval_add, ph, qh], },
+  { intros n a,
+    simp only [←monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial,
+      mul_one, pow_succ', mul_assoc], }
+end
+
+@[simp] lemma eval_mul_X_pow {k : ℕ} : (p * X^k).eval x = p.eval x * x^k :=
+begin
+  induction k with k ih,
+  { simp, },
+  { simp [pow_succ', ←mul_assoc, ih], }
+end
+
 lemma eval_sum (p : polynomial R) (f : ℕ → R → polynomial R) (x : R) :
   (p.sum f).eval x = p.sum (λ n a, (f n a).eval x) :=
 eval₂_sum _ _ _ _
@@ -311,6 +371,9 @@ end
 
 @[simp] lemma C_comp : (C a).comp p = C a := eval₂_C _ _
 
+@[simp] lemma nat_cast_comp {n : ℕ} : (n : polynomial R).comp p = n :=
+by rw [←C_eq_nat_cast, C_comp]
+
 @[simp] lemma comp_zero : p.comp (0 : polynomial R) = C (p.eval 0) :=
 by rw [← C_0, comp_C]
 
@@ -325,6 +388,40 @@ by rw [← C_1, C_comp]
 
 @[simp] lemma add_comp : (p + q).comp r = p.comp r + q.comp r := eval₂_add _ _
 
+@[simp] lemma monomial_comp (n : ℕ) : (monomial n a).comp p = C a * p^n :=
+eval₂_monomial _ _
+
+@[simp] lemma mul_X_comp : (p * X).comp r = p.comp r * r :=
+begin
+  apply polynomial.induction_on' p,
+  { intros p q hp hq, simp [hp, hq, add_mul], },
+  { intros n b, simp [pow_succ', mul_assoc], }
+end
+
+@[simp] lemma X_pow_comp {k : ℕ} : (X^k).comp p = p^k :=
+begin
+  induction k with k ih,
+  { simp, },
+  { simp [pow_succ', mul_X_comp, ih], },
+end
+
+@[simp] lemma mul_X_pow_comp {k : ℕ} : (p * X^k).comp r = p.comp r * r^k :=
+begin
+  induction k with k ih,
+  { simp, },
+  { simp [ih, pow_succ', ←mul_assoc, mul_X_comp], },
+end
+
+@[simp] lemma C_mul_comp : (C a * p).comp r = C a * p.comp r :=
+begin
+  apply polynomial.induction_on' p,
+  { intros p q hp hq, simp [hp, hq, mul_add], },
+  { intros n b, simp [mul_assoc], }
+end
+
+@[simp] lemma nat_cast_mul_comp {n : ℕ} : ((n : polynomial R) * p).comp r = n * p.comp r :=
+by rw [←C_eq_nat_cast, C_mul_comp, C_eq_nat_cast]
+
 @[simp] lemma mul_comp {R : Type*} [comm_semiring R] (p q r : polynomial R) :
   (p * q).comp r = p.comp r * q.comp r := eval₂_mul _ _
 
@@ -336,22 +433,12 @@ begin
   { simp [pow_succ, ih], },
 end
 
-@[simp] lemma monomial_comp (n : ℕ) : (monomial n a).comp p = C a * p^n :=
-eval₂_monomial _ _
-
 @[simp] lemma bit0_comp : comp (bit0 p : polynomial R) q = bit0 (p.comp q) :=
 by simp only [bit0, add_comp]
 
 @[simp] lemma bit1_comp : comp (bit1 p : polynomial R) q = bit1 (p.comp q) :=
 by simp only [bit1, add_comp, bit0_comp, one_comp]
 
-@[simp] lemma cast_nat_comp (n : ℕ) : comp (n : polynomial R) p = n :=
-begin
-  induction n with n ih,
-  { simp, },
-  { simp [ih], },
-end
-
 lemma comp_assoc {R : Type*} [comm_semiring R] (φ ψ χ : polynomial R) :
   (φ.comp ψ).comp χ = φ.comp (ψ.comp χ) :=
 begin
@@ -510,6 +597,12 @@ lemma map_sum {ι : Type*} (g : ι → polynomial R) (s : finset ι) :
   (∑ i in s, g i).map f = ∑ i in s, (g i).map f :=
 eq.symm $ sum_hom _ _
 
+lemma map_comp (p q : polynomial R) : map f (p.comp q) = (map f p).comp (map f q) :=
+polynomial.induction_on p
+  (by simp)
+  (by simp {contextual := tt})
+  (by simp [pow_succ', ← mul_assoc, polynomial.comp] {contextual := tt})
+
 @[simp]
 lemma eval_zero_map (f : R →+* S) (p : polynomial R) :
   (p.map f).eval 0 = f (p.eval 0) :=
@@ -579,12 +672,27 @@ section eval
 
 variables [comm_semiring R] {p q : polynomial R} {x : R}
 
+lemma eval₂_comp [comm_semiring S] (f : R →+* S) {x : S} :
+  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]
+
 @[simp] lemma eval_mul : (p * q).eval x = p.eval x * q.eval x := eval₂_mul _ _
 
 instance eval.is_semiring_hom : is_semiring_hom (eval x) := eval₂.is_semiring_hom _ _
 
 @[simp] lemma eval_pow (n : ℕ) : (p ^ n).eval x = p.eval x ^ n := eval₂_pow _ _ _
 
+@[simp]
+lemma eval_comp : (p.comp q).eval x = p.eval (q.eval x) :=
+begin
+  apply polynomial.induction_on' p,
+  { intros r s hr hs, simp [add_comp, hr, hs], },
+  { intros n a, simp, }
+end
+
+instance comp.is_semiring_hom : is_semiring_hom (λ q : polynomial R, q.comp p) :=
+by unfold comp; apply_instance
+
 lemma eval₂_hom [comm_semiring S] (f : R →+* S) (x : R) :
   p.eval₂ f (f x) = f (p.eval x) :=
 (ring_hom.comp_id f) ▸ (hom_eval₂ p (ring_hom.id R) f x).symm
@@ -637,12 +745,6 @@ begin
   exact ring_hom.map_zero f,
 end
 
-lemma map_comp (p q : polynomial R) : map f (p.comp q) = (map f p).comp (map f q) :=
-polynomial.induction_on p
-  (by simp)
-  (by simp {contextual := tt})
-  (by simp [pow_succ', ← mul_assoc, polynomial.comp] {contextual := tt})
-
 end map
 
 end comm_semiring

src/data/polynomial/monomial.lean

@@ -43,6 +43,12 @@ lemma C_add : C (a + b) = C a + C b := C.map_add a b
 
 lemma C_pow : C (a ^ n) = C a ^ n := C.map_pow a n
 
+@[simp] lemma C_mul_monomial : C a * monomial n b = monomial n (a * b) :=
+by simp only [←monomial_zero_left, monomial_mul_monomial, zero_add]
+
+@[simp] lemma monomial_mul_C : monomial n a * C b = monomial n (a * b) :=
+by simp only [←monomial_zero_left, monomial_mul_monomial, add_zero]
+
 @[simp]
 lemma C_eq_nat_cast (n : ℕ) : C (n : R) = (n : polynomial R) :=
 C.map_nat_cast n