Commit 2023-06-22 13:19 358faa81

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Matrix.lean

Created Mathlib/Analysis/NormedSpace/MatrixExponential.lean

added theorem Matrix.IsHermitian.exp

added theorem Matrix.IsSymm.exp

added theorem Matrix.exp_blockDiagonal'

added theorem Matrix.exp_blockDiagonal

added theorem Matrix.exp_conj'

added theorem Matrix.exp_conj

added theorem Matrix.exp_conjTranspose

added theorem Matrix.exp_diagonal

added theorem Matrix.exp_neg

added theorem Matrix.exp_transpose

added theorem Matrix.exp_units_conj'

added theorem Matrix.exp_zsmul

Modified Mathlib/Data/Matrix/Basic.lean

Modified Mathlib/Topology/Algebra/Ring/Basic.lean