char is some prime given prime is zero

Stream: Is there code for X?

[Joseph Hua]

lemma ring_char_of_prime_eq_zero
  {A : Type*} [non_assoc_semiring A] [nontrivial A]
  {p : ℕ} (hprime : nat.prime p) (hp0 : (p : A) = 0) :
  ring_char A = p :=
begin
  have hchar : ring_char A ∣ p := ring_char.dvd hp0,
  unfold nat.prime at hprime,
  have heq := hprime.2 (ring_char A) hchar,
  cases heq,
  { exfalso,
    exact char_p.ring_char_ne_one heq },
  { exact heq },
end

Is there code for this?

[Eric Rodriguez]

don't think there is

[Eric Rodriguez]

for your last cases or.resolve_{left,right} may help with the golf but this would be nice in mathlib, somewhere within char_p.basic probably

[Joseph Hua]

Cool, will do :) ~Also I probably will add something for character of algebras~ nevermind I found it