Theorems · Theorem · linear algebra

Matrix.exp_transpose

∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommRing 𝔸]
  [inst_3 : TopologicalSpace 𝔸] [inst_4 : IsTopologicalRing 𝔸] [Algebra ℚ 𝔸] [T2Space 𝔸] (A : Matrix m m 𝔸),
  NormedSpace.exp A.transpose = (NormedSpace.exp A).transpose

Defined in: Mathlib.Analysis.Normed.Algebra.MatrixExponential
Cited by: 1 results in Mathlib
Foundations: Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DecidableEq CommRing TopologicalSpace IsTopologicalRing Algebra T2Space

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Fintypestatement and proof · cited by 7,736
Matrixstatement and proof · cited by 4,303
SummationFilter.unconditionalproof · cited by 2,068
T2Spacestatement and proof · cited by 1,351
tsumproof · cited by 1,148
Nat.factorialproof · cited by 616
IsTopologicalRingstatement and proof · cited by 402
Matrix.transposestatement and proof · cited by 389
NormedSpace.expstatement · cited by 157

Cited by1

Results whose statement or proof uses this declaration.

Matrix.IsSymm.expproof · cited by 0