degree_C_mul_T_ite — Mathlib

English

For any R, DecidableEq, n ∈ ℤ, and a ∈ R, deg(C a · T^n) equals if a = 0 then ⊥ else n.

Русский

Для любых R, DecidableEq, n ∈ ℤ и a ∈ R, deg(C a · T^n) равно ⊥, если a = 0, иначе n.

LaTeX

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

Lean4

theorem degree_C_mul_T_ite [DecidableEq R] (n : ℤ) (a : R) : degree (C a * T n) = if a = 0 then ⊥ else ↑n := by
  split_ifs with h <;> simp only [h, map_zero, zero_mul, degree_zero, degree_C_mul_T, Ne, not_false_iff]

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