Theorem Matrix.exp_blockDiagonal'

Modification history

2026-01-06 16:13

Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean

refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` (#30706) …

Modified Matrix.exp_blockDiagonal'View on Github →

2023-06-22 13:19

Mathlib/Analysis/NormedSpace/MatrixExponential.lean

feat: port Analysis.NormedSpace.MatrixExponential (#5381)

Added Matrix.exp_blockDiagonal'View on Github →