R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
⊢ ∀ (x : ℕ), ↑x = 0 ↔ n ∣ x
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
⊢ ∀ (x : ℕ), ↑x = 0 ↔ n ∣ x
have H : (n : R) = 0 := by rw [← hn, CharP.cast_card_eq_zero]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑k = 0 ↔ n ∣ k
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
⊢ ∀ (x : ℕ), ↑x = 0 ↔ n ∣ x
intro k
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑k = 0 → n ∣ k

case mpr
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ n ∣ k → ↑k = 0
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑k = 0 ↔ n ∣ k
constructor
no goals
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
⊢ ↑n = 0
rw [← hn, CharP.cast_card_eq_zero]
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑k = 0
⊢ n ∣ k
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑k = 0 → n ∣ k
intro h
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ n ∣ k
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑k = 0
⊢ n ∣ k
rw [← Nat.mod_add_div k n, Nat.cast_add, Nat.cast_mul, H, MulZeroClass.zero_mul,
  add_zero] at h
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ k % n = 0
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ n ∣ k
rw [Nat.dvd_iff_mod_eq_zero]
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ n > 0
case mp
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ k % n = 0
apply hR _ (Nat.mod_lt _ _) h
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ Nonempty R
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ n > 0
rw [← hn, gt_iff_lt, Fintype.card_pos_iff]
no goals
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
h : ↑(k % n) = 0
⊢ Nonempty R
exact ⟨0⟩
case mpr.intro
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑(n * k) = 0
case mpr
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ n ∣ k → ↑k = 0
rintro ⟨k, rfl⟩
no goals
case mpr.intro
R : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : Fintype R
n : ℕ
hn : Fintype.card R = n
hR : ∀ (i : ℕ), i < n → ↑i = 0 → i = 0
H : ↑n = 0
k : ℕ
⊢ ↑(n * k) = 0
rw [Nat.cast_mul, H, MulZeroClass.zero_mul]