theorem proved term proof

`neg_eq_self`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  78@[simp] theorem neg_eq_self (v : F2Power D) : -v = v := rfl

Term-mode proof.

  79
  80/-- Subtraction reduces to addition in characteristic 2. -/
  81instance : Sub (F2Power D) := ⟨fun u v => u + v⟩
  82

Lean names referenced from this declaration's body.