support_finSuccEquiv_nonempty — Mathlib

English

If f is nonzero, then the support of finSuccEquiv(R,n) f is nonempty.

Русский

Если f не нулевой, то опора finSuccEquiv(R,n) f не пуста.

LaTeX

$$$\\text{If } f \\neq 0, \\; (\\operatorname{finSuccEquiv} R n f).\\operatorname{support}.Nonempty$$$

Lean4

theorem support_finSuccEquiv_nonempty {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) :
    (finSuccEquiv R n f).support.Nonempty := by rwa [Polynomial.support_nonempty, EmbeddingLike.map_ne_zero_iff]

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