case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ mk K p (Nat.zero, 0) = 0

case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (Nat.succ n, 0) = 0
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
⊢ mk K p (n, 0) = 0
induction' n with n ih
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (Nat.succ n, 0) = mk K p (n, 0)
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (Nat.succ n, 0) = 0
rw [← ih]
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n, 0) = mk K p (Nat.succ n, 0)
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (Nat.succ n, 0) = mk K p (n, 0)
symm
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ R K p (n, 0) (Nat.succ n, 0)
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ mk K p (n, 0) = mk K p (Nat.succ n, 0)
apply Quot.sound
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
this : R K p (n, 0) (n + 1, ↑(frobenius K p) 0)
⊢ R K p (n, 0) (Nat.succ n, 0)
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
⊢ R K p (n, 0) (Nat.succ n, 0)
have := R.intro (p := p) n (0 : K)
no goals
case succ.a
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
n : ℕ
ih : mk K p (n, 0) = 0
this : R K p (n, 0) (n + 1, ↑(frobenius K p) 0)
⊢ R K p (n, 0) (Nat.succ n, 0)
rwa [frobenius_zero K p] at this
no goals
case zero
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ mk K p (Nat.zero, 0) = 0
rfl