sq_add_sq_ne_zero — Mathlib

English

If a and b are coprime, then a^2 + b^2 ≠ 0.

Русский

Если a и b взаимно просты, то a^2 + b^2 ≠ 0.

LaTeX

$$$\operatorname{IsCoprime}(a, b) \Rightarrow a^2 + b^2 \neq 0$$$

Lean4

theorem sq_add_sq_ne_zero {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R}
    (h : IsCoprime a b) : a ^ 2 + b ^ 2 ≠ 0 := by
  intro h'
  obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp h'
  obtain rfl := pow_eq_zero ha
  obtain rfl := pow_eq_zero hb
  exact not_isCoprime_zero_zero h

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