no goals
m n : ℕ
h : coprime m n
hmn0 : m * n = 0
⊢ φ (m * n) = φ m * φ n
cases' Nat.mul_eq_zero.1 hmn0 with h h <;>
  simp only [totient_zero, MulZeroClass.mul_zero, MulZeroClass.zero_mul, h]
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ φ (m * n) = φ m * φ n
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
⊢ φ (m * n) = φ m * φ n
haveI : NeZero (m * n) := ⟨hmn0⟩
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝ : NeZero (m * n)
this : NeZero m
⊢ φ (m * n) = φ m * φ n
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ φ (m * n) = φ m * φ n
haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ φ (m * n) = φ m * φ n
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝ : NeZero (m * n)
this : NeZero m
⊢ φ (m * n) = φ m * φ n
haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ φ (m * n) = φ m * φ n
simp only [← ZMod.card_units_eq_totient]
no goals
m n : ℕ
h : coprime m n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ
rw [Fintype.card_congr (Units.mapEquiv (ZMod.chineseRemainder h).toMulEquiv).toEquiv,
  Fintype.card_congr (@MulEquiv.prodUnits (ZMod m) (ZMod n) _ _).toEquiv, Fintype.card_prod]