Theorems · Theorem · general topology

summable_matrix_transpose

∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : AddCommMonoid R] [inst_1 : TopologicalSpace R]
  {L : SummationFilter X} {f : X → Matrix m n R}, Summable (fun x => (f x).transpose) L ↔ Summable f L

Defined in

Mathlib.Topology.Instances.Matrix

Cited by

0 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidTopologicalSpace