degree_C_mul_T_le — Mathlib

English

For any n ∈ ℤ and a ∈ R, deg(C a · T^n) ≤ n, with equality when a ≠ 0 and n is nonnegative, otherwise trivial.

Русский

Для любых n ∈ ℤ и a ∈ R, deg(C a · T^n) ≤ n, равенство достигается при a ≠ 0 и n ≥ 0, иначе тривиально.

LaTeX

$$$\forall n \in \mathbb Z, \forall a \in R:\ degree(C(a) \cdot T^{n}) \le n$$$

Lean4

theorem degree_C_mul_T_le (n : ℤ) (a : R) : degree (C a * T n) ≤ n :=
  by
  by_cases a0 : a = 0
  · simp only [a0, map_zero, zero_mul, degree_zero, bot_le]
  · exact (degree_C_mul_T n a a0).le

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