charmatrix_apply_natDegree — Mathlib

English

The degree of the entry charmatrix M(i,j) is at most 1 if i = j and at most 0 otherwise.

Русский

Степень элемента charmatrix M(i,j) не превышает 1 при i = j и не превосходит 0 в противном случае.

LaTeX

$$$$ \\operatorname{natDegree}\\big( \\operatorname{charmatrix}(M)_{i j} \\big) = \\begin{cases}1, & i=j, \\\\ 0, & i \\neq j. \\end{cases} $$$$

Lean4

theorem charmatrix_apply_natDegree [Nontrivial R] (i j : n) : (charmatrix M i j).natDegree = ite (i = j) 1 0 := by
  by_cases h : i = j <;> simp [h]

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