feat(data/polynomial/*): (p * q).trailing_degree = p.trailing_degree + q.trailing_degree (#14384)

We already had a `nat_trailing_degree_mul` lemma, but this PR does things properly, following the analogous results for `degree`. In particular, we now have some useful intermediate results that do not assume `no_zero_divisors`.

Author: tb65536

src/data/polynomial/degree/trailing_degree.lean

@@ -286,6 +286,50 @@ begin
   exact le_trailing_degree_mul,
 end
 
+lemma coeff_mul_nat_trailing_degree_add_nat_trailing_degree :
+  (p * q).coeff (p.nat_trailing_degree + q.nat_trailing_degree) =
+    p.trailing_coeff * q.trailing_coeff :=
+begin
+  rw coeff_mul,
+  refine finset.sum_eq_single (p.nat_trailing_degree, q.nat_trailing_degree) _
+    (λ h, (h (nat.mem_antidiagonal.mpr rfl)).elim),
+  rintro ⟨i, j⟩ h₁ h₂,
+  rw nat.mem_antidiagonal at h₁,
+  by_cases hi : i < p.nat_trailing_degree,
+  { rw [coeff_eq_zero_of_lt_nat_trailing_degree hi, zero_mul] },
+  by_cases hj : j < q.nat_trailing_degree,
+  { rw [coeff_eq_zero_of_lt_nat_trailing_degree hj, mul_zero] },
+  rw not_lt at hi hj,
+  refine (h₂ (prod.ext_iff.mpr _).symm).elim,
+  exact (add_eq_add_iff_eq_and_eq hi hj).mp h₁.symm,
+end
+
+lemma trailing_degree_mul' (h : p.trailing_coeff * q.trailing_coeff ≠ 0) :
+  (p * q).trailing_degree = p.trailing_degree + q.trailing_degree :=
+begin
+  have hp : p ≠ 0 := λ hp, h (by rw [hp, trailing_coeff_zero, zero_mul]),
+  have hq : q ≠ 0 := λ hq, h (by rw [hq, trailing_coeff_zero, mul_zero]),
+  refine le_antisymm _ le_trailing_degree_mul,
+  rw [trailing_degree_eq_nat_trailing_degree hp, trailing_degree_eq_nat_trailing_degree hq],
+  apply le_trailing_degree_of_ne_zero,
+  rwa coeff_mul_nat_trailing_degree_add_nat_trailing_degree,
+end
+
+lemma nat_trailing_degree_mul' (h : p.trailing_coeff * q.trailing_coeff ≠ 0) :
+  (p * q).nat_trailing_degree = p.nat_trailing_degree + q.nat_trailing_degree :=
+begin
+  have hp : p ≠ 0 := λ hp, h (by rw [hp, trailing_coeff_zero, zero_mul]),
+  have hq : q ≠ 0 := λ hq, h (by rw [hq, trailing_coeff_zero, mul_zero]),
+  apply nat_trailing_degree_eq_of_trailing_degree_eq_some,
+  rw [trailing_degree_mul' h, with_top.coe_add,
+      ←trailing_degree_eq_nat_trailing_degree hp, ←trailing_degree_eq_nat_trailing_degree hq],
+end
+
+lemma nat_trailing_degree_mul [no_zero_divisors R] (hp : p ≠ 0) (hq : q ≠ 0) :
+  (p * q).nat_trailing_degree = p.nat_trailing_degree + q.nat_trailing_degree :=
+nat_trailing_degree_mul' (mul_ne_zero (mt trailing_coeff_eq_zero.mp hp)
+  (mt trailing_coeff_eq_zero.mp hq))
+
 end semiring
 
 section nonzero_semiring

src/data/polynomial/mirror.lean

@@ -160,7 +160,7 @@ variables {R : Type*} [ring R] (p q : R[X])
 lemma mirror_neg : (-p).mirror = -(p.mirror) :=
 by rw [mirror, mirror, reverse_neg, nat_trailing_degree_neg, neg_mul_eq_neg_mul]
 
-variables [is_domain R]
+variables [no_zero_divisors R]
 
 lemma mirror_mul_of_domain : (p * q).mirror = p.mirror * q.mirror :=
 begin
@@ -181,7 +181,7 @@ end ring
 
 section comm_ring
 
-variables {R : Type*} [comm_ring R] [is_domain R] {f : R[X]}
+variables {R : Type*} [comm_ring R] [no_zero_divisors R] {f : R[X]}
 
 lemma irreducible_of_mirror (h1 : ¬ is_unit f)
   (h2 : ∀ k, f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror)

src/data/polynomial/ring_division.lean

@@ -110,6 +110,17 @@ by rw [← with_bot.coe_eq_coe, ← degree_eq_nat_degree (mul_ne_zero hp hq),
     with_bot.coe_add, ← degree_eq_nat_degree hp,
     ← degree_eq_nat_degree hq, degree_mul]
 
+lemma trailing_degree_mul : (p * q).trailing_degree = p.trailing_degree + q.trailing_degree :=
+begin
+  by_cases hp : p = 0,
+  { rw [hp, zero_mul, trailing_degree_zero, top_add] },
+  by_cases hq : q = 0,
+  { rw [hq, mul_zero, trailing_degree_zero, add_top] },
+  rw [trailing_degree_eq_nat_trailing_degree hp, trailing_degree_eq_nat_trailing_degree hq,
+      trailing_degree_eq_nat_trailing_degree (mul_ne_zero hp hq),
+      nat_trailing_degree_mul hp hq, with_top.coe_add],
+end
+
 @[simp] lemma nat_degree_pow (p : R[X]) (n : ℕ) :
   nat_degree (p ^ n) = n * nat_degree p :=
 if hp0 : p = 0
@@ -161,16 +172,6 @@ instance : is_domain R[X] :=
 { ..polynomial.no_zero_divisors,
   ..polynomial.nontrivial, }
 
-lemma nat_trailing_degree_mul (hp : p ≠ 0) (hq : q ≠ 0) :
-  (p * q).nat_trailing_degree = p.nat_trailing_degree + q.nat_trailing_degree :=
-begin
-  simp only [←tsub_eq_of_eq_add_rev (nat_degree_eq_reverse_nat_degree_add_nat_trailing_degree _)],
-  rw [reverse_mul_of_domain, nat_degree_mul hp hq, nat_degree_mul (mt reverse_eq_zero.mp hp)
-    (mt reverse_eq_zero.mp hq), reverse_nat_degree, reverse_nat_degree, tsub_add_eq_tsub_tsub,
-    nat.add_comm, add_tsub_assoc_of_le (nat.sub_le _ _), add_comm,
-    add_tsub_assoc_of_le (nat.sub_le _ _)],
-end
-
 end ring
 
 section comm_ring