coeff_rename_ne_zero — Mathlib

English

If (rename f φ).coeff d ≠ 0, then there exists u with u.mapDomain f = d and φ.coeff u ≠ 0.

Русский

Если (rename f φ).coeff d ≠ 0, то существует u с u.mapDomain f = d и φ.coeff u ≠ 0.

LaTeX

$$$ (rename f φ).\mathrm{coeff}\ d \neq 0 \Rightarrow \exists u, u.\mapDomain f = d \land φ.\mathrm{coeff} u \neq 0 $$$

Lean4

theorem coeff_rename_ne_zero (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ) (h : (rename f φ).coeff d ≠ 0) :
    ∃ u : σ →₀ ℕ, u.mapDomain f = d ∧ φ.coeff u ≠ 0 :=
  by
  contrapose! h
  apply coeff_rename_eq_zero _ _ _ h

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