eq_self_iff_eq_zero_of_char_ne_two

English

In a domain with characteristic not equal to two, we have -a = a iff a = 0.

Русский

В домене с характеристикой ≠ 2 имеем -a = a тогда и только тогда, когда a = 0.

LaTeX

$$$ (-a = a) \iff a = 0 $ under\ CharZero\_condition$$

Lean4

/-- Characteristic `≠ 2` in a domain implies that `-a = a` iff `a = 0`. -/
theorem eq_self_iff_eq_zero_of_char_ne_two {R : Type*} [NonAssocRing R] [Nontrivial R] [NoZeroDivisors R]
    (hR : ringChar R ≠ 2) {a : R} : -a = a ↔ a = 0 :=
  ⟨fun h => (mul_eq_zero.mp <| (two_mul a).trans <| neg_eq_iff_add_eq_zero.mp h).resolve_left (Ring.two_ne_zero hR),
    fun h => ((congr_arg (fun x => -x) h).trans neg_zero).trans h.symm⟩

Похожие утверждения