ne_zero — Mathlib

English

For a finite 2-ary function p valued in R, if p(0) and p(1) are coprime, then p is not the zero function.

Русский

Если p(0) и p(1) взаимно просты, то функция p не является нулевой.

LaTeX

$$$IsCoprime(p(0),p(1)) \Rightarrow p \neq 0$$$

Lean4

/-- If a 2-vector `p` satisfies `IsCoprime (p 0) (p 1)`, then `p ≠ 0`. -/
theorem ne_zero [Nontrivial R] {p : Fin 2 → R} (h : IsCoprime (p 0) (p 1)) : p ≠ 0 :=
  by
  rintro rfl
  exact not_isCoprime_zero_zero h

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