matrix_transpose — Mathlib

English

A simple criterion: Summable of the transposed matrices is equivalent to Summable of the original matrices.

Русский

Условие: суммируемость транспонированных матриц эквивалентна суммируемости исходных матриц.

LaTeX

$$$\\text{Summable}(f^T,L) \\iff \\text{Summable}(f,L)$$$

Lean4

theorem matrix_transpose {f : X → Matrix m n R} {a : Matrix m n R} (hf : HasSum f a L) :
    HasSum (fun x => (f x)ᵀ) aᵀ L :=
  (hf.map (Matrix.transposeAddEquiv m n R) continuous_id.matrix_transpose :)

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