feat(LinearAlgebra/Matrix/Block, Analysis/Normed/Algebra/MatrixExponential): add BlockTriangular.pow and BlockTriangular.exp (#37006)

These will help with proving  `det (exp A) = exp (trace A)`

Zulip thread: 
[#new members > (Matrix and NormedSpace.exp) | det (exp A) = exp (trace A)](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/.28Matrix.20and.20NormedSpace.2Eexp.29.20.7C.20det.20.28exp.20A.29.20.3D.20exp.20.28trace.20A.29/with/580964688)

Co-authored-by: hakii6 <hakii6@hakii6.localdomain>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <efw@google.com>

Author: 3 people

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

@@ -10,7 +10,9 @@ public import Mathlib.Analysis.Matrix.Normed
 public import Mathlib.LinearAlgebra.Matrix.ZPow
 public import Mathlib.LinearAlgebra.Matrix.Hermitian
 public import Mathlib.LinearAlgebra.Matrix.Symmetric
+public import Mathlib.LinearAlgebra.Matrix.Block
 public import Mathlib.Topology.UniformSpace.Matrix
+public import Mathlib.Topology.Instances.Matrix
 
 /-!
 # Lemmas about the matrix exponential
@@ -67,7 +69,7 @@ open scoped Matrix
 
 open NormedSpace -- For `exp`.
 
-variable {m n : Type*} {n' : m → Type*} {𝔸 : Type*}
+variable {m n : Type*} {n' : m → Type*} {α 𝔸 : Type*}
 
 namespace Matrix
 
@@ -98,6 +100,11 @@ theorem IsHermitian.exp [StarRing 𝔸] [ContinuousStar 𝔸] {A : Matrix m m 
     (exp A).IsHermitian :=
   (exp_conjTranspose _).symm.trans <| congr_arg _ h
 
+theorem BlockTriangular.exp [LinearOrder α] [Algebra ℚ 𝔸] {M : Matrix m m 𝔸} {b : m → α}
+    (hM : BlockTriangular M b) :
+    (exp M).BlockTriangular b :=
+  exp_mem (s := blockTriangularSubalgebra ℚ _ b) isClosed_setOf_blockTriangular hM
+
 end Ring
 
 section CommRing

Mathlib/LinearAlgebra/Matrix/Block.lean

@@ -44,7 +44,7 @@ open Matrix
 universe v
 
 variable {α β m n o : Type*} {m' n' : α → Type*}
-variable {R : Type v} {M N : Matrix m m R} {b : m → α}
+variable {R : Type v} {A : Type*} {M N : Matrix m m R} {b : m → α}
 
 namespace Matrix
 
@@ -186,6 +186,44 @@ theorem BlockTriangular.mul [Fintype m] [NonUnitalNonAssocSemiring R]
   · simp_rw [hM hki, zero_mul]
   · simp_rw [hN (lt_of_lt_of_le hij hki), mul_zero]
 
+variable (R b) in
+/-- `BlockTriangular` matrices form a subsemiring. -/
+@[simps]
+def blockTriangularSubsemiring [DecidableEq m] [Fintype m] [Semiring R] :
+    Subsemiring (Matrix m m R) where
+  carrier := {M | BlockTriangular M b}
+  zero_mem' := blockTriangular_zero
+  one_mem' := blockTriangular_one
+  mul_mem' := .mul
+  add_mem' := .add
+
+@[simp]
+theorem mem_blockTriangularSubsemiring [DecidableEq m] [Fintype m] [Semiring R]
+    {M : Matrix m m R} :
+    M ∈ blockTriangularSubsemiring R b ↔ BlockTriangular M b :=
+  Iff.rfl
+
+theorem BlockTriangular.pow [DecidableEq m] [Fintype m] [Semiring R] (hM : BlockTriangular M b)
+    (n : ℕ) : BlockTriangular (M ^ n) b :=
+  pow_mem (S := blockTriangularSubsemiring R b) hM n
+
+theorem blockTriangular_algebraMap [CommSemiring R] [Semiring A] [Algebra R A]
+    [DecidableEq m] [Fintype m] (r : R) : (algebraMap R (Matrix m m A) r).BlockTriangular b :=
+  blockTriangular_diagonal _
+
+variable (R A b) in
+/-- `BlockTriangular` matrices form a subalgebra. -/
+def blockTriangularSubalgebra [CommSemiring R] [Semiring A] [Algebra R A]
+    [DecidableEq m] [Fintype m] : Subalgebra R (Matrix m m A) where
+  __ := blockTriangularSubsemiring A b
+  algebraMap_mem' r := blockTriangular_algebraMap r
+
+@[simp]
+theorem mem_blockTriangularSubalgebra [CommSemiring R] [Semiring A] [Algebra R A]
+    [DecidableEq m] [Fintype m] {M : Matrix m m A} :
+    M ∈ blockTriangularSubalgebra R A b ↔ BlockTriangular M b :=
+  Iff.rfl
+
 end LinearOrder
 
 theorem upper_two_blockTriangular [Zero R] [Preorder α] (A : Matrix m m R) (B : Matrix m n R)

Mathlib/Topology/Instances/Matrix.lean

@@ -6,6 +6,7 @@ Authors: Oliver Nash, Eric Wieser
 module
 
 public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
+public import Mathlib.LinearAlgebra.Matrix.Block
 public import Mathlib.Topology.Algebra.InfiniteSum.Basic
 public import Mathlib.Topology.Algebra.Ring.Basic
 public import Mathlib.Topology.Algebra.Star
@@ -307,6 +308,12 @@ theorem Continuous.matrix_blockDiag'
     Continuous fun x => blockDiag' (A x) :=
   continuous_pi fun _i => continuous_matrix fun _j _k => hA.matrix_elem _ _
 
+theorem isClosed_setOf_blockTriangular {α : Type*} {b : m → α} [LinearOrder α] [Zero R]
+    [T2Space R] : IsClosed {M : Matrix m m R | M.BlockTriangular b} := by
+  simp only [BlockTriangular, Set.setOf_forall]
+  refine isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun _ => ?_
+  exact isClosed_eq (continuous_id.matrix_elem i j) continuous_const
+
 end BlockMatrices
 
 end Continuity