teaching module about charP

Stream: new members

[Yakov Pechersky]

Would it be possible to extend the module tactic to know about char p rings? Example:

import Mathlib

lemma foo (a k : ZMod 2) : a - k + a = k := by
  have : (2 : ZMod 2) = 0 := rfl
  success_if_fail_with_msg "ring failed, ring expressions not equal
a k : ZMod 2
this : 2 = 0
⊢ 2 = 0" module
  sorry