nontrivial_of_nontrivial — Mathlib

English

There exist two distinct polynomials in MvPolynomial σ R when R is nontrivial.

Русский

Существуют два различных полинома в MvPolynomial σ R, когда R ненулевой.

LaTeX

$$$ \exists p,q : MvPolynomial\; \sigma\; R,\ p \neq q $$$

Lean4

instance nontrivial_of_nontrivial (σ : Type*) (R : Type*) [CommSemiring R] [Nontrivial R] :
    Nontrivial (MvPolynomial σ R) :=
  inferInstanceAs (Nontrivial <| AddMonoidAlgebra R (σ →₀ ℕ))

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