Theorems · Theorem · general topology

Matrix.transpose_tsum

∀ {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} [T2Space R] {f : X → Matrix m n R},
  (∑'[L] (x : X), f x).transpose = ∑'[L] (x : X), (f x).transpose

Defined in

Mathlib.Topology.Instances.Matrix

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidTopologicalSpaceT2Space