support_C_mul_T — Mathlib

English

For any DecidableEq R, integers n and elements a ∈ R, the degree of C a · T^n is equal to if a = 0 then ⊥ else n.

Русский

Для любого DecidableEq R, целого n и элемента a ∈ R, степень C a · T^n равна 0⊥, если a = 0, иначе n.

LaTeX

$$$\forall [\DecidableEq R] (n : \mathbb Z) (a : R):\ degree(C(a) \cdot T^{n}) = \operatorname{ite}(a = 0) (\bot) (↑n)$$$

Lean4

theorem support_C_mul_T (a : R) (n : ℤ) : Finsupp.support (C a * T n) ⊆ { n } :=
  by
  rw [← single_eq_C_mul_T]
  exact support_single_subset

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