feat(data/polynomial): irreducible_of_irreducible_mod_prime (#3539)

I was waiting on this, an exercise from Johan's tutorial at LftCM, to see if a participant would PR it. Perhaps not, so I'll contribute this now.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

src/data/polynomial/ring_division.lean

@@ -322,6 +322,67 @@ end
 
 end integral_domain
 
+section
+
+variables [semiring R] [integral_domain S] (φ : R →+* S)
+
+lemma is_unit_of_is_unit_leading_coeff_of_is_unit_map
+  (f : polynomial R) (hf : is_unit (leading_coeff f)) (H : is_unit (map φ f)) :
+  is_unit f :=
+begin
+  have dz := degree_eq_zero_of_is_unit H,
+  rw degree_map_eq_of_leading_coeff_ne_zero at dz,
+  { rw eq_C_of_degree_eq_zero dz,
+    apply is_unit.map',
+    convert hf,
+    rw (degree_eq_iff_nat_degree_eq _).1 dz,
+    rintro rfl,
+    simpa using H, },
+  { intro h,
+    have u : is_unit (φ f.leading_coeff) := is_unit.map' _ hf,
+    rw h at u,
+    simpa using u, }
+end
+
+end
+
+section
+variables [integral_domain R] [integral_domain S] (φ : R →+* S)
+/--
+A polynomial over an integral domain `R` is irreducible if it is monic and
+  irreducible after mapping into an integral domain `S`.
+
+A special case of this lemma is that a polynomial over `ℤ` is irreducible if
+  it is monic and irreducible over `ℤ/pℤ` for some prime `p`.
+-/
+lemma irreducible_of_irreducible_map (f : polynomial R)
+  (h_mon : monic f) (h_irr : irreducible (map φ f)) :
+  irreducible f :=
+begin
+  fsplit,
+  { intro h,
+    exact h_irr.1 (is_unit.map (monoid_hom.of (map φ)) h), },
+  { intros a b h,
+
+    have q := (leading_coeff_mul a b).symm,
+    rw ←h at q,
+    dsimp [monic] at h_mon,
+    rw h_mon at q,
+    have au : is_unit a.leading_coeff := is_unit_of_mul_eq_one _ _ q,
+    rw mul_comm at q,
+    have bu : is_unit b.leading_coeff := is_unit_of_mul_eq_one _ _ q,
+    clear q h_mon,
+
+    have h' := congr_arg (map φ) h,
+    simp only [map_mul] at h',
+    cases h_irr.2 _ _ h' with w w,
+    { left,
+      exact is_unit_of_is_unit_leading_coeff_of_is_unit_map _ _ au w, },
+    { right,
+      exact is_unit_of_is_unit_leading_coeff_of_is_unit_map _ _ bu w, }, }
+end
+
+end
 
 end polynomial