feat(data/nat/totient): totient_mul (#8441)

Also made `data/nat/totient` import `data/zmod/basic` instead of the other way round because I think people are more likely to want `zmod` but not `totient` than `totient` but not `zmod`.

Also deleted the deprecated `gpowers` because it caused a name clash in `group_theory/subgroup` when the imports were changed.

src/data/nat/totient.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import algebra.big_operators.basic
+import data.zmod.basic
 
 /-!
 # Euler's totient function
@@ -36,6 +37,42 @@ lemma totient_pos : ∀ {n : ℕ}, 0 < n → 0 < φ n
 | 1 := by simp [totient]
 | (n+2) := λ h, card_pos.2 ⟨1, mem_filter.2 ⟨mem_range.2 dec_trivial, coprime_one_right _⟩⟩
 
+open zmod
+
+@[simp] lemma _root_.zmod.card_units_eq_totient (n : ℕ) [fact (0 < n)] :
+  fintype.card (units (zmod n)) = φ n :=
+calc fintype.card (units (zmod n)) = fintype.card {x : zmod n // x.val.coprime n} :
+  fintype.card_congr zmod.units_equiv_coprime
+... = φ n :
+begin
+  apply finset.card_congr (λ (a : {x : zmod n // x.val.coprime n}) _, a.1.val),
+  { intro a, simp [(a : zmod n).val_lt, a.prop.symm] {contextual := tt} },
+  { intros _ _ _ _ h, rw subtype.ext_iff_val, apply val_injective, exact h, },
+  { intros b hb,
+    rw [finset.mem_filter, finset.mem_range] at hb,
+    refine ⟨⟨b, _⟩, finset.mem_univ _, _⟩,
+    { let u := unit_of_coprime b hb.2.symm,
+      exact val_coe_unit_coprime u },
+    { show zmod.val (b : zmod n) = b,
+      rw [val_nat_cast, nat.mod_eq_of_lt hb.1], } }
+end
+
+lemma totient_mul {m n : ℕ} (h : m.coprime n) : φ (m * n) = φ m * φ n :=
+if hmn0 : m * n = 0
+  then by cases nat.mul_eq_zero.1 hmn0 with h h;
+    simp only [totient_zero, mul_zero, zero_mul, h]
+  else
+  begin
+    haveI : fact (0 < (m * n)) := ⟨nat.pos_of_ne_zero hmn0⟩,
+    haveI : fact (0 < m) := ⟨nat.pos_of_ne_zero $ left_ne_zero_of_mul hmn0⟩,
+    haveI : fact (0 < n) := ⟨nat.pos_of_ne_zero $ right_ne_zero_of_mul hmn0⟩,
+    rw [← zmod.card_units_eq_totient, ← zmod.card_units_eq_totient,
+      ← zmod.card_units_eq_totient,
+      fintype.card_congr (units.map_equiv (chinese_remainder h).to_mul_equiv).to_equiv,
+      fintype.card_congr (@mul_equiv.prod_units (zmod m) (zmod n) _ _).to_equiv,
+      fintype.card_prod]
+  end
+
 lemma sum_totient (n : ℕ) : ∑ m in (range n.succ).filter (∣ n), φ m = n :=
 if hn0 : n = 0 then by simp [hn0]
 else

src/data/zmod/basic.lean

@@ -6,7 +6,6 @@ Authors: Chris Hughes
 
 import data.int.modeq
 import algebra.char_p.basic
-import data.nat.totient
 import ring_theory.ideal.operations
 import tactic.fin_cases
 
@@ -586,7 +585,7 @@ def units_equiv_coprime {n : ℕ} [fact (0 < n)] :
   right_inv := λ ⟨_, _⟩, by simp }
 
 /-- The **Chinese remainder theorem**. For a pair of coprime natural numbers, `m` and `n`,
-  the rings `zmod (m * n)` and `zmod m × zmod n` are isomorphic. 
+  the rings `zmod (m * n)` and `zmod m × zmod n` are isomorphic.
 
 See `ideal.quotient_inf_ring_equiv_pi_quotient` for the Chinese remainder theorem for ideals in any
 ring.
@@ -633,29 +632,6 @@ have inv : function.left_inverse inv_fun to_fun ∧ function.right_inverse inv_f
   left_inv := inv.1,
   right_inv := inv.2 }
 
-section totient
-open_locale nat
-
-@[simp] lemma card_units_eq_totient (n : ℕ) [fact (0 < n)] :
-  fintype.card (units (zmod n)) = φ n :=
-calc fintype.card (units (zmod n)) = fintype.card {x : zmod n // x.val.coprime n} :
-  fintype.card_congr zmod.units_equiv_coprime
-... = φ n :
-begin
-  apply finset.card_congr (λ (a : {x : zmod n // x.val.coprime n}) _, a.1.val),
-  { intro a, simp [(a : zmod n).val_lt, a.prop.symm] {contextual := tt} },
-  { intros _ _ _ _ h, rw subtype.ext_iff_val, apply val_injective, exact h, },
-  { intros b hb,
-    rw [finset.mem_filter, finset.mem_range] at hb,
-    refine ⟨⟨b, _⟩, finset.mem_univ _, _⟩,
-    { let u := unit_of_coprime b hb.2.symm,
-      exact val_coe_unit_coprime u },
-    { show zmod.val (b : zmod n) = b,
-      rw [val_nat_cast, nat.mod_eq_of_lt hb.1], } }
-end
-
-end totient
-
 instance subsingleton_units : subsingleton (units (zmod 2)) :=
 ⟨λ x y, begin
   ext1,

src/deprecated/subgroup.lean

@@ -121,39 +121,6 @@ lemma is_subgroup_Union_of_directed {ι : Type*} [hι : nonempty ι]
     set.mem_Union.2 ⟨i, is_subgroup.inv_mem hi⟩,
   to_is_submonoid := is_submonoid_Union_of_directed s directed }
 
-def gpowers (x : G) : set G := set.range ((^) x : ℤ → G)
-def gmultiples (x : A) : set A := set.range (λ i, gsmul i x)
-attribute [to_additive gmultiples] gpowers
-
-instance gpowers.is_subgroup (x : G) : is_subgroup (gpowers x) :=
-{ one_mem := ⟨(0:ℤ), by simp⟩,
-  mul_mem := assume x₁ x₂ ⟨i₁, h₁⟩ ⟨i₂, h₂⟩, ⟨i₁ + i₂, by simp [gpow_add, *]⟩,
-  inv_mem := assume x₀ ⟨i, h⟩, ⟨-i, by simp [h.symm]⟩ }
-
-instance gmultiples.is_add_subgroup (x : A) : is_add_subgroup (gmultiples x) :=
-multiplicative.is_subgroup_iff.1 $ gpowers.is_subgroup _
-attribute [to_additive] gpowers.is_subgroup
-
-lemma is_subgroup.gpow_mem {a : G} {s : set G} [is_subgroup s] (h : a ∈ s) : ∀{i:ℤ}, a ^ i ∈ s
-| (n : ℕ) := by { rw [gpow_coe_nat], exact is_submonoid.pow_mem h }
-| -[1+ n] := by { rw [gpow_neg_succ_of_nat], exact is_subgroup.inv_mem (is_submonoid.pow_mem h) }
-
-lemma is_add_subgroup.gsmul_mem {a : A} {s : set A} [is_add_subgroup s] :
-  a ∈ s → ∀{i:ℤ}, gsmul i a ∈ s :=
-@is_subgroup.gpow_mem (multiplicative A) _ _ _ (multiplicative.is_subgroup _)
-
-lemma gpowers_subset {a : G} {s : set G} [is_subgroup s] (h : a ∈ s) : gpowers a ⊆ s :=
-λ x hx, match x, hx with _, ⟨i, rfl⟩ := is_subgroup.gpow_mem h end
-
-lemma gmultiples_subset {a : A} {s : set A} [is_add_subgroup s] (h : a ∈ s) : gmultiples a ⊆ s :=
-@gpowers_subset (multiplicative A) _ _ _ (multiplicative.is_subgroup _) h
-
-attribute [to_additive gmultiples_subset] gpowers_subset
-
-lemma mem_gpowers {a : G} : a ∈ gpowers a := ⟨1, by simp⟩
-lemma mem_gmultiples {a : A} : a ∈ gmultiples a := ⟨1, by simp⟩
-attribute [to_additive mem_gmultiples] mem_gpowers
-
 end group
 
 namespace is_subgroup
@@ -576,12 +543,6 @@ begin
     rw [mul_assoc, mul_assoc, mul_left_comm yt] }
 end
 
-@[to_additive gmultiples_eq_closure]
-theorem gpowers_eq_closure {a : G} : gpowers a = closure {a} :=
-subset.antisymm
-  (gpowers_subset $ mem_closure $ by simp)
-  (closure_subset $ by simp [mem_gpowers])
-
 end group
 
 namespace is_subgroup

src/linear_algebra/free_module_pid.lean

@@ -277,7 +277,7 @@ begin
   { obtain ⟨P, P_eq, P_max⟩ := set_has_maximal_iff_noetherian.mpr
         (infer_instance : is_noetherian R R) _ (submodule.range_map_nonempty N),
     obtain ⟨ϕ, rfl⟩ := set.mem_range.mp P_eq,
-    use ϕ,
+    existsi ϕ,
     intros ψ hψ,
     exact P_max (N.map ψ) ⟨_, rfl⟩ hψ },
   let ϕ := this.some,