support_C_mul_T_of_ne_zero — Mathlib

English

If a ≠ 0, then the degree of C a · T^n is exactly n (as a singleton degree).

Русский

Если a ≠ 0, то степень C a · T^n ровно равна n (как единственный элемент степени).

LaTeX

$$$\forall {R} {a : R} {n : \mathbb Z},\ a \neq 0 \Rightarrow\ degree(C(a) \cdot T^{n}) = \{ n \}$$$

Lean4

theorem support_C_mul_T_of_ne_zero {a : R} (a0 : a ≠ 0) (n : ℤ) : Finsupp.support (C a * T n) = { n } :=
  by
  rw [← single_eq_C_mul_T]
  exact support_single_ne_zero _ a0

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