eq_zero_of_mul_self_add_mul_self_eq_zero

English

Let R be a linearly ordered ring with no zero divisors. If a^2 + b^2 = 0, then a = 0 (and hence b = 0 as well).

Русский

Пусть R — упорядоченное кольцо без делителей нуля. Если a^2 + b^2 = 0, то a = 0 (и, следовательно, b = 0).

LaTeX

$$$$a^2 + b^2 = 0 \\;\\Rightarrow\\; a = 0,$$$$

Lean4

theorem eq_zero_of_mul_self_add_mul_self_eq_zero [NoZeroDivisors R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R]
    (h : a * a + b * b = 0) : a = 0 :=
  (mul_self_add_mul_self_eq_zero.mp h).left

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