mul_self_add_mul_self_eq_zero — Mathlib

English

NoZeroDivisors plus existing add-le properties imply a^2 + b^2 = 0 iff a = 0 ∧ b = 0.

Русский

При отсутствии нулейразделителей и свойствах аккуратного сложения имеем a^2 + b^2 = 0 ↔ a = 0 ∧ b = 0.

LaTeX

$$$a^2 + b^2 = 0 \iff a = 0 \land b = 0$$$

Lean4

/-- The sum of two squares is zero iff both elements are zero. -/
theorem mul_self_add_mul_self_eq_zero [NoZeroDivisors R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] :
    a * a + b * b = 0 ↔ a = 0 ∧ b = 0 := by
  rw [add_eq_zero_iff_of_nonneg, mul_self_eq_zero (M₀ := R), mul_self_eq_zero (M₀ := R)] <;> apply mul_self_nonneg

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