Theorem: IMOSL.Extra.CharTwo.Semiring_of_two_eq_zero (IMOSLLean4/Extra/CharTwo/Ring/Basic.lean)

State before:
R : Type u_1
inst✝ : NonAssocSemiring R
h : 2 = 0
x : R
⊢ x + x = 0
Tactic:
rw [← two_mul, h, zero_mul]
State after:
no goals