natDegree_monomial — Mathlib

English

For [DecidableEq R], natDegree (monomial i r) equals i if r ≠ 0, otherwise 0.

Русский

При наличии разрешимости равенства natDegree (monomial i r) = i, если r ≠ 0, иначе 0.

LaTeX

$$natDegree(monomial i r) = if r = 0 then 0 else i$$

Lean4

@[simp]
theorem natDegree_monomial [DecidableEq R] (i : ℕ) (r : R) : natDegree (monomial i r) = if r = 0 then 0 else i :=
  by
  split_ifs with hr
  · simp [hr]
  · rw [← C_mul_X_pow_eq_monomial, natDegree_C_mul_X_pow i r hr]

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