Theorem: Model.Field.ringChar_eq_of_Prime (ECTate/Algebra/EllipticCurve/Model.lean)

State before:
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : OfNat.ofNat n = 0
hnp : Nat.Prime n
⊢ ringChar K = n
Tactic:
rw [← Nat.cast_eq_ofNat, ringChar.spec] at hn
State after:
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : ringChar K ∣ n
hnp : Nat.Prime n
⊢ ringChar K = n

State before:
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : ringChar K ∣ n
hnp : Nat.Prime n
⊢ ringChar K = n
Tactic:
cases (Nat.dvd_prime hnp).mp hn with
| inl h =>
  simpa [h] using CharP.char_is_prime_or_zero K (ringChar K)
| inr h =>
  assumption
State after:
no goals

State before:
case inl
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : ringChar K ∣ n
hnp : Nat.Prime n
h : ringChar K = 1
⊢ ringChar K = n
Tactic:
simpa [h] using CharP.char_is_prime_or_zero K (ringChar K)
State after:
no goals

State before:
case inr
K : Type u
inst✝¹ : Field K
n : ℕ
inst✝ : Nat.AtLeastTwo n
hn : ringChar K ∣ n
hnp : Nat.Prime n
h : ringChar K = n
⊢ ringChar K = n
Tactic:
assumption
State after:
no goals