feat(ring_theory/polynomial/cyclotomic): generalize a few results to …

…domains (#10741)

Primarily for flt-regular



Co-authored-by: Johan Commelin <johan@commelin.net>

src/data/multiset/basic.lean

@@ -2176,10 +2176,10 @@ theorem count_map_eq_count' [decidable_eq β] (f : α → β) (s : multiset α)
 begin
   by_cases H : x ∈ s,
   { exact count_map_eq_count f _ (set.inj_on_of_injective hf _) _ H, },
-  { simp [H, not_exists, count_eq_zero, count_eq_zero_of_not_mem H, hf],
-    intros y hy hh,
-    apply H,
-    rwa [← hf hh], }
+  { rw [count_eq_zero_of_not_mem H, count_eq_zero, mem_map],
+    rintro ⟨k, hks, hkx⟩,
+    rw hf hkx at *,
+    contradiction }
 end
 
 lemma filter_eq' (s : multiset α) (b : α) : s.filter (= b) = repeat b (count b s) :=

src/data/polynomial/degree/definitions.lean

@@ -911,21 +911,23 @@ by { rw ← degree_neg q at h, rw [sub_eq_add_neg, degree_add_eq_right_of_degree
 end ring
 
 section nonzero_ring
-variables [nontrivial R] [ring R]
+variables [nontrivial R]
 
-@[simp] lemma degree_X_sub_C (a : R) : degree (X - C a) = 1 :=
+@[simp] lemma degree_X_add_C [semiring R] (a : R) : degree (X + C a) = 1 :=
 have degree (C a) < degree (X : polynomial R),
 from calc degree (C a) ≤ 0 : degree_C_le
                    ... < 1 : with_bot.some_lt_some.mpr zero_lt_one
                    ... = degree X : degree_X.symm,
-by rw [degree_sub_eq_left_of_degree_lt this, degree_X]
+by rw [degree_add_eq_left_of_degree_lt this, degree_X]
+
+variables [ring R]
 
-@[simp] lemma degree_X_add_C (a : R) : degree (X + C a) = 1 :=
+@[simp] lemma degree_X_sub_C (a : R) : degree (X - C a) = 1 :=
 have degree (C a) < degree (X : polynomial R),
 from calc degree (C a) ≤ 0 : degree_C_le
                    ... < 1 : with_bot.some_lt_some.mpr zero_lt_one
                    ... = degree X : degree_X.symm,
-by rw [degree_add_eq_left_of_degree_lt this, degree_X]
+by rw [degree_sub_eq_left_of_degree_lt this, degree_X]
 
 @[simp] lemma nat_degree_X_sub_C (x : R) : (X - C x).nat_degree = 1 :=
 nat_degree_eq_of_degree_eq_some $ degree_X_sub_C x

src/data/polynomial/field_division.lean

@@ -25,7 +25,10 @@ universes u v w y z
 variables {R : Type u} {S : Type v} {k : Type y} {A : Type z} {a b : R} {n : ℕ}
 
 section is_domain
-variables [comm_ring R] [is_domain R] [normalization_monoid R]
+variables [comm_ring R] [is_domain R]
+
+section normalization_monoid
+variables [normalization_monoid R]
 
 instance : normalization_monoid (polynomial R) :=
 { norm_unit := λ p, ⟨C ↑(norm_unit (p.leading_coeff)), C ↑(norm_unit (p.leading_coeff))⁻¹,
@@ -57,6 +60,31 @@ lemma monic.normalize_eq_self {p : polynomial R} (hp : p.monic) :
 by simp only [polynomial.coe_norm_unit, normalize_apply, hp.leading_coeff, norm_unit_one,
   units.coe_one, polynomial.C.map_one, mul_one]
 
+end normalization_monoid
+
+lemma prod_multiset_root_eq_finset_root {p : polynomial R} :
+  (multiset.map (λ (a : R), X - C a) p.roots).prod =
+  ∏ a in p.roots.to_finset, (X - C a) ^ root_multiplicity a p :=
+by simp only [count_roots, finset.prod_multiset_map_count]
+
+lemma roots_C_mul (p : polynomial R) {a : R} (hzero : a ≠ 0) : (C a * p).roots = p.roots :=
+begin
+  by_cases hpzero : p = 0,
+  { simp only [hpzero, mul_zero] },
+  rw multiset.ext,
+  intro b,
+  have prodzero : C a * p ≠ 0,
+  { simp only [hpzero, or_false, ne.def, mul_eq_zero, C_eq_zero, hzero, not_false_iff] },
+  rw [count_roots, count_roots, root_multiplicity_mul prodzero],
+  have mulzero : root_multiplicity b (C a) = 0,
+  { simp only [hzero, root_multiplicity_eq_zero, eval_C, is_root.def, not_false_iff] },
+  simp only [mulzero, zero_add]
+end
+
+lemma roots_normalize [normalization_monoid R] {p : polynomial R} : (normalize p).roots = p.roots :=
+by rw [normalize_apply, mul_comm, coe_norm_unit,
+  roots_C_mul _ (norm_unit (leading_coeff p)).ne_zero]
+
 end is_domain
 
 section division_ring
@@ -432,11 +460,6 @@ begin
   rw [← C_inj, this, C_0],
 end
 
-lemma prod_multiset_root_eq_finset_root {R : Type*} [comm_ring R] [is_domain R] {p : polynomial R} :
-  (multiset.map (λ (a : R), X - C a) p.roots).prod =
-  ∏ a in p.roots.to_finset, (X - C a) ^ root_multiplicity a p :=
-by simp only [count_roots, finset.prod_multiset_map_count]
-
 /-- The product `∏ (X - a)` for `a` inside the multiset `p.roots` divides `p`. -/
 lemma prod_multiset_X_sub_C_dvd (p : polynomial R) :
   (multiset.map (λ (a : R), X - C a) p.roots).prod ∣ p :=
@@ -452,25 +475,5 @@ begin
   exact pow_root_multiplicity_dvd p a
 end
 
-lemma roots_C_mul {R : Type*} [comm_ring R] [is_domain R] (p : polynomial R) {a : R}
-  (hzero : a ≠ 0) : (C a * p).roots = p.roots :=
-begin
-  by_cases hpzero : p = 0,
-  { simp only [hpzero, mul_zero] },
-  rw multiset.ext,
-  intro b,
-  have prodzero : C a * p ≠ 0,
-  { simp only [hpzero, or_false, ne.def, mul_eq_zero, C_eq_zero, hzero, not_false_iff] },
-  rw [count_roots, count_roots, root_multiplicity_mul prodzero],
-  have mulzero : root_multiplicity b (C a) = 0,
-  { simp only [hzero, root_multiplicity_eq_zero, eval_C, is_root.def, not_false_iff] },
-  simp only [mulzero, zero_add]
-end
-
-lemma roots_normalize {R : Type*} [comm_ring R] [is_domain R] [normalization_monoid R]
-  {p : polynomial R} : (normalize p).roots = p.roots :=
-by rw [normalize_apply, mul_comm, coe_norm_unit,
-  roots_C_mul _ (norm_unit (leading_coeff p)).ne_zero]
-
 end field
 end polynomial

src/field_theory/splitting_field.lean

@@ -375,7 +375,7 @@ end
 
 /-- A monic polynomial `p` that has as many roots as its degree
 can be written `p = ∏(X - a)`, for `a` in `p.roots`. -/
-lemma prod_multiset_X_sub_C_of_monic_of_roots_card_eq_of_field {p : polynomial K}
+private lemma prod_multiset_X_sub_C_of_monic_of_roots_card_eq_of_field {p : polynomial K}
   (hmonic : p.monic) (hroots : p.roots.card = p.nat_degree) :
   (multiset.map (λ (a : K), X - C a) p.roots).prod = p :=
 begin
@@ -426,7 +426,7 @@ end
 /-- A polynomial `p` that has as many roots as its degree
 can be written `p = p.leading_coeff * ∏(X - a)`, for `a` in `p.roots`.
 Used to prove the more general `C_leading_coeff_mul_prod_multiset_X_sub_C` below. -/
-lemma C_leading_coeff_mul_prod_multiset_X_sub_C_of_field {p : polynomial K}
+private lemma C_leading_coeff_mul_prod_multiset_X_sub_C_of_field {p : polynomial K}
   (hroots : p.roots.card = p.nat_degree) :
   C p.leading_coeff * (multiset.map (λ (a : K), X - C a) p.roots).prod = p :=
 begin

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -132,27 +132,27 @@ lemma roots_of_cyclotomic (n : ℕ) (R : Type*) [comm_ring R] [is_domain R] :
   (cyclotomic' n R).roots = (primitive_roots n R).val :=
 by { rw cyclotomic', exact roots_prod_X_sub_C (primitive_roots n R) }
 
-end is_domain
-
-section field
-
-variables {K : Type*} [field K]
-
 /-- If there is a primitive `n`th root of unity in `K`, then `X ^ n - 1 = ∏ (X - μ)`, where `μ`
 varies over the `n`-th roots of unity. -/
-lemma X_pow_sub_one_eq_prod {ζ : K} {n : ℕ} (hpos : 0 < n) (h : is_primitive_root ζ n) :
-  X ^ n - 1 = ∏ ζ in nth_roots_finset n K, (X - C ζ) :=
+lemma X_pow_sub_one_eq_prod {ζ : R} {n : ℕ} (hpos : 0 < n) (h : is_primitive_root ζ n) :
+  X ^ n - 1 = ∏ ζ in nth_roots_finset n R, (X - C ζ) :=
 begin
   rw [nth_roots_finset, ← multiset.to_finset_eq (is_primitive_root.nth_roots_nodup h)],
   simp only [finset.prod_mk, ring_hom.map_one],
   rw [nth_roots],
-  have hmonic : (X ^ n - C (1 : K)).monic := monic_X_pow_sub_C (1 : K) (ne_of_lt hpos).symm,
+  have hmonic : (X ^ n - C (1 : R)).monic := monic_X_pow_sub_C (1 : R) (ne_of_lt hpos).symm,
   symmetry,
   apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic,
-  rw [@nat_degree_X_pow_sub_C K _ _ n 1, ← nth_roots],
+  rw [@nat_degree_X_pow_sub_C R _ _ n 1, ← nth_roots],
   exact is_primitive_root.card_nth_roots h
 end
 
+end is_domain
+
+section field
+
+variables {K : Type*} [field K]
+
 /-- `cyclotomic' n K` splits. -/
 lemma cyclotomic'_splits (n : ℕ) : splits (ring_hom.id K) (cyclotomic' n K) :=
 begin
@@ -169,8 +169,8 @@ by rw [splits_iff_card_roots, ← nth_roots, is_primitive_root.card_nth_roots h,
 
 /-- If there is a primitive `n`-th root of unity in `K`, then
 `∏ i in nat.divisors n, cyclotomic' i K = X ^ n - 1`. -/
-lemma prod_cyclotomic'_eq_X_pow_sub_one {ζ : K} {n : ℕ} (hpos : 0 < n) (h : is_primitive_root ζ n) :
-  ∏ i in nat.divisors n, cyclotomic' i K = X ^ n - 1 :=
+lemma prod_cyclotomic'_eq_X_pow_sub_one {K : Type*} [comm_ring K] [is_domain K] {ζ : K} {n : ℕ}
+  (hpos : 0 < n) (h : is_primitive_root ζ n) : ∏ i in nat.divisors n, cyclotomic' i K = X ^ n - 1 :=
 begin
   rw [X_pow_sub_one_eq_prod hpos h],
   have rwcyc : ∀ i ∈ nat.divisors n, cyclotomic' i K = ∏ μ in primitive_roots i K, (X - C μ),
@@ -187,7 +187,8 @@ end
 
 /-- If there is a primitive `n`-th root of unity in `K`, then
 `cyclotomic' n K = (X ^ k - 1) /ₘ (∏ i in nat.proper_divisors k, cyclotomic' i K)`. -/
-lemma cyclotomic'_eq_X_pow_sub_one_div {ζ : K} {n : ℕ} (hpos: 0 < n) (h : is_primitive_root ζ n) :
+lemma cyclotomic'_eq_X_pow_sub_one_div {K : Type*} [comm_ring K] [is_domain K] {ζ : K} {n : ℕ}
+  (hpos : 0 < n) (h : is_primitive_root ζ n) :
   cyclotomic' n K = (X ^ n - 1) /ₘ (∏ i in nat.proper_divisors n, cyclotomic' i K) :=
 begin
   rw [←prod_cyclotomic'_eq_X_pow_sub_one hpos h,
@@ -207,9 +208,10 @@ end
 
 /-- If there is a primitive `n`-th root of unity in `K`, then `cyclotomic' n K` comes from a
 monic polynomial with integer coefficients. -/
-lemma int_coeff_of_cyclotomic' {ζ : K} {n : ℕ} (h : is_primitive_root ζ n) :
+lemma int_coeff_of_cyclotomic' {K : Type*} [comm_ring K] [is_domain K] {ζ : K} {n : ℕ}
+  (h : is_primitive_root ζ n) :
   (∃ (P : polynomial ℤ), map (int.cast_ring_hom K) P = cyclotomic' n K ∧
-  P.degree = (cyclotomic' n K).degree ∧ P.monic) :=
+    P.degree = (cyclotomic' n K).degree ∧ P.monic) :=
 begin
   refine lifts_and_degree_eq_and_monic _ (cyclotomic'.monic n K),
   induction n using nat.strong_induction_on with k hk generalizing ζ h,
@@ -249,7 +251,8 @@ end
 
 /-- If `K` is of characteristic `0` and there is a primitive `n`-th root of unity in `K`,
 then `cyclotomic n K` comes from a unique polynomial with integer coefficients. -/
-lemma unique_int_coeff_of_cycl [char_zero K] {ζ : K} {n : ℕ+} (h : is_primitive_root ζ n) :
+lemma unique_int_coeff_of_cycl {K : Type*} [comm_ring K] [is_domain K] [char_zero K] {ζ : K}
+  {n : ℕ+} (h : is_primitive_root ζ n) :
   (∃! (P : polynomial ℤ), map (int.cast_ring_hom K) P = cyclotomic' n K) :=
 begin
   obtain ⟨P, hP⟩ := int_coeff_of_cyclotomic' h,
@@ -473,8 +476,8 @@ end
 /-- If there is a primitive `n`-th root of unity in `K`, then
 `cyclotomic n K = ∏ μ in primitive_roots n R, (X - C μ)`. In particular,
 `cyclotomic n K = cyclotomic' n K` -/
-lemma cyclotomic_eq_prod_X_sub_primitive_roots {K : Type*} [field K] {ζ : K} {n : ℕ}
-  (hz : is_primitive_root ζ n) :
+lemma cyclotomic_eq_prod_X_sub_primitive_roots {K : Type*} [comm_ring K] [is_domain K] {ζ : K}
+  {n : ℕ} (hz : is_primitive_root ζ n) :
   cyclotomic n K = ∏ μ in primitive_roots n K, (X - C μ) :=
 begin
   rw ←cyclotomic',
@@ -494,14 +497,9 @@ end
 lemma is_root_cyclotomic {n : ℕ} {K : Type*} [comm_ring K] [is_domain K] (hpos : 0 < n) {μ : K}
   (h : is_primitive_root μ n) : is_root (cyclotomic n K) μ :=
 begin
-  suffices : is_root (cyclotomic n (fraction_ring K)) (algebra_map K (fraction_ring K) μ),
-  { rw [←map_cyclotomic n (algebra_map K (fraction_ring K))] at this,
-    apply is_root.of_map this,
-    exact is_fraction_ring.injective K (fraction_ring K) },
-  replace h := h.map_of_injective (is_fraction_ring.injective K (fraction_ring K)),
-  rw [← mem_roots (cyclotomic_ne_zero n (fraction_ring K)),
+  rw [← mem_roots (cyclotomic_ne_zero n K),
       cyclotomic_eq_prod_X_sub_primitive_roots h, roots_prod_X_sub_C, ← finset.mem_def],
-  rwa [← mem_primitive_roots hpos] at h
+  rwa [← mem_primitive_roots hpos] at h,
 end
 
 private lemma is_root_cyclotomic_iff' {n : ℕ} {K : Type*} [field K] {μ : K} (hn : (n : K) ≠ 0) :

src/ring_theory/roots_of_unity.lean

@@ -856,7 +856,8 @@ section minpoly
 
 open minpoly
 
-variables {n : ℕ} {K : Type*} [field K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n)
+section comm_ring
+variables {n : ℕ} {K : Type*} [comm_ring K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n)
 
 include n μ h hpos
 
@@ -869,6 +870,11 @@ begin
   { simp only [((is_primitive_root.iff_def μ n).mp h).left, eval₂_one, eval₂_X_pow, eval₂_sub,
       sub_self] }
 end
+end comm_ring
+
+variables {n : ℕ} {K : Type*} [field K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n)
+
+include n μ h hpos
 
 variables [char_zero K]