Characteristic 3 of GF(3): x + x + x = 0
ProvedTrit.char3In the field GF(3) = ZMod 3, every element has additive order dividing 3: x + x + x = 0. Agda proof of record: Sovereign.Algebra.ChainZ3toZ12.char3-triple (type-theory presentation-group base, Trit = GF(3)).
Preamble
import Mathlib
Formal statement
theorem Trit.char3 (x : ZMod 3) : x + x + x = 0 := by sorry
Source