degree_C_ite — Mathlib

English

For DecidableEq R, the degree of C a is determined by whether a equals 0: it is ⊥ if a = 0, otherwise 0.

Русский

Для DecidableEq R степень C a определяется по тому, равен ли a нулю: ⊥ если a = 0, иначе 0.

LaTeX

$$$\forall a \in R\ [\DecidableEq R],\ (C a).degree = \text{ite}(a = 0) (\bot) (0)$$$

Lean4

theorem degree_C_ite [DecidableEq R] (a : R) : (C a).degree = if a = 0 then ⊥ else 0 := by
  split_ifs with h <;> simp only [h, map_zero, degree_zero, degree_C, Ne, not_false_iff]

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