infinite_of_nonempty — Mathlib

English

If σ is nonempty and R is infinite, then MvPolynomial σ R is infinite.

Русский

Если индексы σ непусты и R бесконечна, то MvPolynomial σ R бесконечен.

LaTeX

$$$ Infinite(\MvPolynomial\; σ\; R) $$$

Lean4

instance infinite_of_nonempty (σ : Type*) (R : Type*) [Nonempty σ] [CommSemiring R] [Nontrivial R] :
    Infinite (MvPolynomial σ R) :=
  Infinite.of_injective ((fun s : σ →₀ ℕ => monomial s 1) ∘ Finsupp.single (Classical.arbitrary σ)) <|
    (monomial_left_injective one_ne_zero).comp (Finsupp.single_injective _)

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