From 974d23c227e98c8f5d65abcbc16777f44192a34b Mon Sep 17 00:00:00 2001
From: Alex J Best <alex.j.best@gmail.com>
Date: Sat, 5 Mar 2022 17:38:12 +0000
Subject: [PATCH] feat(data/polynomial/monic): add
 monic_of_mul_monic_left/right (#12446)

Also clean up variables that are defined in the section.

From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60geom_sum.20.28X.20.20n.29.60.20is.20monic/near/274130839
---
 src/data/polynomial/monic.lean | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

diff --git a/src/data/polynomial/monic.lean b/src/data/polynomial/monic.lean
index 32001558a74b9..6944691ec950e 100644
--- a/src/data/polynomial/monic.lean
+++ b/src/data/polynomial/monic.lean
@@ -26,7 +26,7 @@ variables {R : Type u} {S : Type v} {a b : R} {m n : ℕ} {ι : Type y}
 section semiring
 variables [semiring R] {p q r : R[X]}
 
-lemma monic.as_sum {p : R[X]} (hp : p.monic) :
+lemma monic.as_sum (hp : p.monic) :
   p = X^(p.nat_degree) + (∑ i in range p.nat_degree, C (p.coeff i) * X^i) :=
 begin
   conv_lhs { rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm] },
@@ -93,14 +93,28 @@ lemma monic_pow (hp : monic p) : ∀ (n : ℕ), monic (p ^ n)
 | 0     := monic_one
 | (n+1) := by { rw pow_succ, exact monic_mul hp (monic_pow n) }
 
-lemma monic_add_of_left {p q : R[X]} (hp : monic p) (hpq : degree q < degree p) :
+lemma monic_add_of_left (hp : monic p) (hpq : degree q < degree p) :
   monic (p + q) :=
 by rwa [monic, add_comm, leading_coeff_add_of_degree_lt hpq]
 
-lemma monic_add_of_right {p q : R[X]} (hq : monic q) (hpq : degree p < degree q) :
+lemma monic_add_of_right (hq : monic q) (hpq : degree p < degree q) :
   monic (p + q) :=
 by rwa [monic, leading_coeff_add_of_degree_lt hpq]
 
+lemma monic.of_mul_monic_left (hp : p.monic) (hpq : (p * q).monic) : q.monic :=
+begin
+  contrapose! hpq,
+  rw monic.def at hpq ⊢,
+  rwa leading_coeff_monic_mul hp,
+end
+
+lemma monic.of_mul_monic_right (hq : q.monic) (hpq : (p * q).monic) : p.monic :=
+begin
+  contrapose! hpq,
+  rw monic.def at hpq ⊢,
+  rwa leading_coeff_mul_monic hq,
+end
+
 namespace monic
 
 @[simp]