degree_C_mul_T — Mathlib

English

For any n ∈ ℤ and a ∈ R with a ≠ 0, deg(C a · T^n) = some n (i.e., the degree is the exponent n).

Русский

Для любого n ∈ ℤ и a ∈ R, если a ≠ 0, степень C a · T^n равна n.

LaTeX

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

Lean4

@[simp]
theorem degree_C_mul_T (n : ℤ) (a : R) (a0 : a ≠ 0) : degree (C a * T n) = n :=
  by
  rw [degree, support_C_mul_T_of_ne_zero a0 n]
  exact Finset.max_singleton

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