diag_sum — Mathlib

English

The diagonal of a finite sum of matrices equals the sum of the diagonals: diag(∑ f i) = ∑ diag(f i).

Русский

Диагональ суммы матриц равна сумме диагоналей: diag(∑ f i) = ∑ diag(f i).

LaTeX

$$$\\operatorname{diag}\\left(\\sum_{i} f(i)\\right) = \\sum_{i} \\operatorname{diag}(f(i))$$$

Lean4

@[simp]
theorem diag_sum {ι} [AddCommMonoid α] (s : Finset ι) (f : ι → Matrix n n α) :
    diag (∑ i ∈ s, f i) = ∑ i ∈ s, diag (f i) :=
  map_sum (diagAddMonoidHom n α) f s

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