Commit 2026-05-20 06:13 421fab31

View on Github →

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)

Estimated changes

Modified Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

added theorem Matrix.BlockTriangular.exp

Modified Mathlib/LinearAlgebra/Matrix/Block.lean

added theorem Matrix.BlockTriangular.pow

added def Matrix.blockTriangularSubalgebra

added def Matrix.blockTriangularSubsemiring

added theorem Matrix.blockTriangular_algebraMap

added theorem Matrix.mem_blockTriangularSubalgebra

added theorem Matrix.mem_blockTriangularSubsemiring

Modified Mathlib/Topology/Instances/Matrix.lean

added theorem isClosed_setOf_blockTriangular