case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ Nat.zero
a b : ZMod Nat.zero
⊢ ↑(a * b) = ↑a * ↑b

case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑(a * b) = ↑a * ↑b
n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
a b : ZMod n
⊢ ↑(a * b) = ↑a * ↑b
cases n
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑a * ↑b = ↑(a * b)
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑(a * b) = ↑a * ↑b
symm
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑(val a) * ↑(val b) = ↑(val (a * b))
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑a * ↑b = ↑(a * b)
dsimp [ZMod, ZMod.cast]
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ m ∣ val a * val b - val a * val b % Nat.succ n✝
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ ↑(val a) * ↑(val b) = ↑(val (a * b))
erw [← Nat.cast_mul, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
  @CharP.cast_eq_zero_iff R _ m]
no goals
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ Nat.succ n✝
a b : ZMod (Nat.succ n✝)
⊢ m ∣ val a * val b - val a * val b % Nat.succ n✝
exact h.trans (Nat.dvd_sub_mod _)
no goals
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ Nat.zero
a b : ZMod Nat.zero
⊢ ↑(a * b) = ↑a * ↑b
apply Int.cast_mul