vars_C_mul — Mathlib

English

Multiplication by a nonzero constant does not change the set of variables.

Русский

Умножение на ненулевую константу не изменяет множество переменных.

LaTeX

$$$$ (C a * \varphi).\mathrm{vars} = \varphi.\mathrm{vars} \quad (a \neq 0) $$$$

Lean4

theorem vars_C_mul (a : A) (ha : a ≠ 0) (φ : MvPolynomial σ A) : (C a * φ : MvPolynomial σ A).vars = φ.vars :=
  by
  ext1 i
  simp only [mem_vars, mem_support_iff]
  apply exists_congr
  intro d
  rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and]

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