Topological properties of matrices

This file is a place to collect topological results about matrices.

Main definitions

• Matrix.topologicalRing: square matrices form a topological ring

Main results

• Sets of matrices:
  • IsOpen.matrix: the set of finite matrices with entries in an open set is itself an open set.
  • IsCompact.matrix: the set of matrices with entries in a compact set is itself a compact set.
• Continuity:
  • Continuous.matrix_det: the determinant is continuous over a topological ring.
  • Continuous.matrix_adjugate: the adjugate is continuous over a topological ring.
• Infinite sums
  • Matrix.transpose_tsum: transpose commutes with infinite sums
  • Matrix.diagonal_tsum: diagonal commutes with infinite sums
  • Matrix.blockDiagonal_tsum: block diagonal commutes with infinite sums
  • Matrix.blockDiagonal'_tsum: non-uniform block diagonal commutes with infinite sums

@[instance_reducible]

instance instTopologicalSpaceMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] : TopologicalSpace (Matrix m n R)

Equations

• instTopologicalSpaceMatrix = instTopologicalSpaceMatrix._aux_1

instance instT2SpaceMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [T2Space R] : T2Space (Matrix m n R)

instance instDiscreteTopologyMatrixOfFinite {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Finite m] [Finite n] [DiscreteTopology R] : DiscreteTopology (Matrix m n R)

The topology on finite matrices over a discrete space is discrete.

theorem IsOpen.matrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [Finite m] [Finite n] [TopologicalSpace R] {S : Set R} (hS : IsOpen S) : IsOpen S.matrix

theorem IsCompact.matrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] {S : Set R} (hS : IsCompact S) : IsCompact S.matrix

Lemmas about continuity of operations

instance instContinuousConstSMulMatrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [SMul α R] [ContinuousConstSMul α R] : ContinuousConstSMul α (Matrix m n R)

instance instContinuousSMulMatrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [TopologicalSpace α] [SMul α R] [ContinuousSMul α R] : ContinuousSMul α (Matrix m n R)

instance instContinuousAddMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Add R] [ContinuousAdd R] : ContinuousAdd (Matrix m n R)

instance instContinuousNegMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Neg R] [ContinuousNeg R] : ContinuousNeg (Matrix m n R)

instance instIsTopologicalAddGroupMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [AddGroup R] [IsTopologicalAddGroup R] : IsTopologicalAddGroup (Matrix m n R)

theorem continuous_matrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [TopologicalSpace α] {f : α → Matrix m n R} (h : ∀ (i : m) (j : n), Continuous fun (a : α) => f a i j) : Continuous f

To show a function into matrices is continuous it suffices to show the coefficients of the resulting matrix are continuous

theorem Continuous.matrix_elem {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix m n R} (hA : Continuous A) (i : m) (j : n) : Continuous fun (x : X) => A x i j

theorem continuous_matrixOf {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [TopologicalSpace α] {f : α → m → n → R} : (Continuous fun (x : α) => Matrix.of (f x)) ↔ Continuous f

theorem Continuous.matrixOf {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [TopologicalSpace α] {f : α → m → n → R} : Continuous f → Continuous fun (x : α) => Matrix.of (f x)

Alias of the reverse direction of continuous_matrixOf.

theorem Continuous.matrix_map {X : Type u_1} {m : Type u_4} {n : Type u_5} {S : Type u_7} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [TopologicalSpace S] {A : X → Matrix m n S} {f : S → R} (hA : Continuous A) (hf : Continuous f) : Continuous fun (x : X) => (A x).map f

theorem Continuous.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix m n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).transpose

theorem Continuous.matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Star R] [ContinuousStar R] {A : X → Matrix m n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).conjTranspose

instance instContinuousStarMatrix {m : Type u_4} {R : Type u_8} [TopologicalSpace R] [Star R] [ContinuousStar R] : ContinuousStar (Matrix m m R)

theorem Continuous.matrix_replicateCol {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {ι : Type u_11} {A : X → n → R} (hA : Continuous A) : Continuous fun (x : X) => Matrix.replicateCol ι (A x)

theorem Continuous.matrix_replicateRow {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {ι : Type u_11} {A : X → n → R} (hA : Continuous A) : Continuous fun (x : X) => Matrix.replicateRow ι (A x)

theorem Continuous.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Zero R] [DecidableEq n] {A : X → n → R} (hA : Continuous A) : Continuous fun (x : X) => Matrix.diagonal (A x)

theorem Continuous.dotProduct {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] {A B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => A x ⬝ᵥ B x

theorem Continuous.matrix_mul {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] {A : X → Matrix m n R} {B : X → Matrix n p R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => A x * B x

For square matrices the usual continuous_mul can be used.

instance instContinuousMulMatrixOfContinuousAdd {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] : ContinuousMul (Matrix n n R)

instance instIsTopologicalSemiringMatrix {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] : IsTopologicalSemiring (Matrix n n R)

instance Matrix.topologicalRing {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [NonUnitalNonAssocRing R] [IsTopologicalRing R] : IsTopologicalRing (Matrix n n R)

theorem Continuous.matrix_vecMulVec {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Mul R] [ContinuousMul R] {A : X → m → R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => Matrix.vecMulVec (A x) (B x)

theorem Continuous.matrix_mulVec {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R] [Fintype n] {A : X → Matrix m n R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => (A x).mulVec (B x)

theorem Continuous.matrix_vecMul {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R] [Fintype m] {A : X → m → R} {B : X → Matrix m n R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => Matrix.vecMul (A x) (B x)

theorem Continuous.matrix_submatrix {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix l n R} (hA : Continuous A) (e₁ : m → l) (e₂ : p → n) : Continuous fun (x : X) => (A x).submatrix e₁ e₂

theorem Continuous.matrix_reindex {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix l n R} (hA : Continuous A) (e₁ : l ≃ m) (e₂ : n ≃ p) : Continuous fun (x : X) => (Matrix.reindex e₁ e₂) (A x)

theorem Continuous.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).diag

theorem continuous_matrix_diag {n : Type u_5} {R : Type u_8} [TopologicalSpace R] : Continuous Matrix.diag

theorem Continuous.matrix_trace {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [AddCommMonoid R] [ContinuousAdd R] {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).trace

theorem Continuous.matrix_det {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).det

theorem Continuous.matrix_updateCol {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [DecidableEq n] (i : n) {A : X → Matrix m n R} {B : X → m → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => (A x).updateCol i (B x)

theorem Continuous.matrix_updateRow {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [DecidableEq m] (i : m) {A : X → Matrix m n R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => (A x).updateRow i (B x)

theorem Continuous.matrix_cramer {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) : Continuous fun (x : X) => (A x).cramer (B x)

theorem Continuous.matrix_adjugate {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun (x : X) => (A x).adjugate

theorem continuousAt_matrix_inv {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] (A : Matrix n n R) (h : ContinuousAt Ring.inverse A.det) : ContinuousAt Inv.inv A

When Ring.inverse is continuous at the determinant (such as in a NormedRing, or a topological field), so is Matrix.inv.

theorem Topology.IsInducing.matrix_map {m : Type u_11} {n : Type u_12} {R : Type u_13} {S : Type u_14} [TopologicalSpace R] [TopologicalSpace S] {f : R → S} (hf : IsInducing f) : IsInducing fun (x : Matrix m n R) => x.map f

theorem Topology.IsEmbedding.matrix_map {m : Type u_11} {n : Type u_12} {R : Type u_13} {S : Type u_14} [TopologicalSpace R] [TopologicalSpace S] {f : R → S} (hf : IsEmbedding f) : IsEmbedding fun (x : Matrix m n R) => x.map f

theorem Topology.IsClosedEmbedding.matrix_map {m : Type u_11} {n : Type u_12} {R : Type u_13} {S : Type u_14} [TopologicalSpace R] [TopologicalSpace S] {f : R → S} (hf : IsClosedEmbedding f) : IsClosedEmbedding fun (x : Matrix m n R) => x.map f

theorem Topology.IsOpenEmbedding.matrix_map {m : Type u_11} {n : Type u_12} {R : Type u_13} {S : Type u_14} [TopologicalSpace R] [TopologicalSpace S] {f : R → S} [Finite m] [Finite n] (hf : IsOpenEmbedding f) : IsOpenEmbedding fun (x : Matrix m n R) => x.map f

theorem Continuous.matrix_fromBlocks {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix n l R} {B : X → Matrix n m R} {C : X → Matrix p l R} {D : X → Matrix p m R} (hA : Continuous A) (hB : Continuous B) (hC : Continuous C) (hD : Continuous D) : Continuous fun (x : X) => Matrix.fromBlocks (A x) (B x) (C x) (D x)

theorem Continuous.matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Zero R] [DecidableEq p] {A : X → p → Matrix m n R} (hA : Continuous A) : Continuous fun (x : X) => Matrix.blockDiagonal (A x)

theorem Continuous.matrix_blockDiag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix (m × p) (n × p) R} (hA : Continuous A) : Continuous fun (x : X) => (A x).blockDiag

theorem Continuous.matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [TopologicalSpace X] [TopologicalSpace R] [Zero R] [DecidableEq l] {A : X → (i : l) → Matrix (m' i) (n' i) R} (hA : Continuous A) : Continuous fun (x : X) => Matrix.blockDiagonal' (A x)

theorem Continuous.matrix_blockDiag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [TopologicalSpace X] [TopologicalSpace R] {A : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R} (hA : Continuous A) : Continuous fun (x : X) => (A x).blockDiag'

theorem isClosed_setOfPred_blockTriangular {m : Type u_4} {R : Type u_8} [TopologicalSpace R] {α : Type u_11} {b : m → α} [LinearOrder α] [Zero R] [T2Space R] : IsClosed {M : Matrix m m R | M.BlockTriangular b}

@[deprecated isClosed_setOfPred_blockTriangular (since := "2026-07-09")]

theorem isClosed_setOf_blockTriangular {m : Type u_4} {R : Type u_8} [TopologicalSpace R] {α : Type u_11} {b : m → α} [LinearOrder α] [Zero R] [T2Space R] : IsClosed {M : Matrix m m R | M.BlockTriangular b}

Alias of isClosed_setOfPred_blockTriangular.

Lemmas about infinite sums

theorem HasSum.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix m n R} {a : Matrix m n R} (hf : HasSum f a L) : HasSum (fun (x : X) => (f x).transpose) a.transpose L

theorem Summable.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix m n R} (hf : Summable f L) : Summable (fun (x : X) => (f x).transpose) L

@[simp]

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

theorem Matrix.transpose_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [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

theorem HasSum.matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} {a : Matrix m n R} (hf : HasSum f a L) : HasSum (fun (x : X) => (f x).conjTranspose) a.conjTranspose L

theorem Summable.matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} (hf : Summable f L) : Summable (fun (x : X) => (f x).conjTranspose) L

@[simp]

theorem summable_matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} : Summable (fun (x : X) => (f x).conjTranspose) L ↔ Summable f L

theorem Matrix.conjTranspose_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [StarAddMonoid R] [ContinuousStar R] [T2Space R] {f : X → Matrix m n R} : (∑'[L] (x : X), f x).conjTranspose = ∑'[L] (x : X), (f x).conjTranspose

theorem HasSum.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq n] {f : X → n → R} {a : n → R} (hf : HasSum f a L) : HasSum (fun (x : X) => Matrix.diagonal (f x)) (Matrix.diagonal a) L

theorem Summable.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq n] {f : X → n → R} (hf : Summable f L) : Summable (fun (x : X) => Matrix.diagonal (f x)) L

@[simp]

theorem summable_matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq n] {f : X → n → R} : Summable (fun (x : X) => Matrix.diagonal (f x)) L ↔ Summable f L

theorem Matrix.diagonal_tsum {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq n] [T2Space R] {f : X → n → R} : diagonal (∑'[L] (x : X), f x) = ∑'[L] (x : X), diagonal (f x)

theorem HasSum.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix n n R} {a : Matrix n n R} (hf : HasSum f a L) : HasSum (fun (x : X) => (f x).diag) a.diag L

theorem Summable.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix n n R} (hf : Summable f L) : Summable (fun (x : X) => (f x).diag) L

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

theorem Summable.matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq p] {f : X → p → Matrix m n R} (hf : Summable f L) : Summable (fun (x : X) => Matrix.blockDiagonal (f x)) L

theorem summable_matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq p] {f : X → p → Matrix m n R} : Summable (fun (x : X) => Matrix.blockDiagonal (f x)) L ↔ Summable f L

theorem Matrix.blockDiagonal_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq p] [T2Space R] {f : X → p → Matrix m n R} : blockDiagonal (∑'[L] (x : X), f x) = ∑'[L] (x : X), blockDiagonal (f x)

theorem HasSum.matrix_blockDiag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix (m × p) (n × p) R} {a : Matrix (m × p) (n × p) R} (hf : HasSum f a L) : HasSum (fun (x : X) => (f x).blockDiag) a.blockDiag L

theorem Summable.matrix_blockDiag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix (m × p) (n × p) R} (hf : Summable f L) : Summable (fun (x : X) => (f x).blockDiag) L

theorem HasSum.matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq l] {f : X → (i : l) → Matrix (m' i) (n' i) R} {a : (i : l) → Matrix (m' i) (n' i) R} (hf : HasSum f a L) : HasSum (fun (x : X) => Matrix.blockDiagonal' (f x)) (Matrix.blockDiagonal' a) L

theorem Summable.matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq l] {f : X → (i : l) → Matrix (m' i) (n' i) R} (hf : Summable f L) : Summable (fun (x : X) => Matrix.blockDiagonal' (f x)) L

theorem summable_matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq l] {f : X → (i : l) → Matrix (m' i) (n' i) R} : Summable (fun (x : X) => Matrix.blockDiagonal' (f x)) L ↔ Summable f L

theorem Matrix.blockDiagonal'_tsum {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} [DecidableEq l] [T2Space R] {f : X → (i : l) → Matrix (m' i) (n' i) R} : blockDiagonal' (∑'[L] (x : X), f x) = ∑'[L] (x : X), blockDiagonal' (f x)

theorem HasSum.matrix_blockDiag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R} {a : Matrix ((i : l) × m' i) ((i : l) × n' i) R} (hf : HasSum f a L) : HasSum (fun (x : X) => (f x).blockDiag') a.blockDiag' L

theorem Summable.matrix_blockDiag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [AddCommMonoid R] [TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R} (hf : Summable f L) : Summable (fun (x : X) => (f x).blockDiag') L