diag_single_same — Mathlib

English

If you take a diagonal matrix with a single nonzero at i, i, then its diagonal equals the scalar Pi.single i c at position i.

Русский

Если диагональная матрица имеет единственный ненулевой элемент в позиции i,i, то её диагональ равна Pi.single i c в позиции i.

LaTeX

$$$ \mathrm{diag}(\mathrm{single}_{i i} c) = \mathrm Pi.single i c $$$

Lean4

@[simp 1050]
theorem diag_single_same : diag (single i i c) = Pi.single i c :=
  by
  ext j
  by_cases hij : i = j <;> (try rw [hij]) <;> simp [hij]

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