of_polynomial_ne — Mathlib

English

If there exist polynomials p ≠ q in Polynomial R, then R is nontrivial.

Русский

Если в полиномах над R существуют различные полиномы p ≠ q, то кольцо R ненулевое.

LaTeX

$$$\exists p,q \in \operatorname{Polynomial}(R), p \neq q \Rightarrow \operatorname{Nontrivial}(R)$$$

Lean4

theorem of_polynomial_ne (h : p ≠ q) : Nontrivial R :=
  (subsingleton_or_nontrivial R).resolve_left fun _hI => h <| Subsingleton.elim _ _

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