Theorems · Theorem · general topology

HasSum.matrix_blockDiagonal

∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} [inst_2 : DecidableEq p] {f : X → p → Matrix m n R}
  {a : p → Matrix m n R}, HasSum f a L → HasSum (fun x => Matrix.blockDiagonal (f x)) (Matrix.blockDiagonal a) L

Defined in

Mathlib.Topology.Instances.Matrix

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidTopologicalSpaceDecidableEq