transpose_tsum — Mathlib

English

The transpose of the sum equals the sum of transposes for the tsum over X.

Русский

Перепределение транспонирования суммы равняется сумме транспонированных, для суммирования по X.

LaTeX

$$$\\bigl(\\sum'_{L} f\\bigr)^T = \\sum'_{L} f^T$$$

Lean4

theorem transpose_tsum [T2Space R] {f : X → Matrix m n R} : (∑'[L] x, f x)ᵀ = ∑'[L] x, (f x)ᵀ :=
  Function.LeftInverse.map_tsum f (g := transposeAddEquiv m n R) continuous_id.matrix_transpose
    continuous_id.matrix_transpose transpose_transpose

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