Physlib.Mathematics.DataStructures.Matrix.LieTrace

Imports

/-
Copyright (c) 2025 Matteo Cipollina. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Matteo Cipollina
-/
module

public import Mathlib.Analysis.Complex.Polynomial.Basic
public import Mathlib.Analysis.Normed.Algebra.MatrixExponential
public import Physlib.Mathematics.SchurTriangulation

Lie's Trace Formula

This file proves the formula det (exp A) = exp (tr A) for matrices, also known as Lie's trace formula.

The proof proceeds by first showing the formula for upper-triangular matrices and then leveraging Schur triangulation to generalize to any matrix. An upper-triangular matrix A is defined in mathlib as Matrix.BlockTriangular A id.

Main results

Matrix.det_exp: The determinant of the exponential of a matrix is the exponential of its trace.

@[expose] public section

instance [UniformSpace 𝕂] : UniformSpace (Matrix m n 𝕂) := by𝕂:Type u_1m:Type u_2n:Type u_3inst✝:UniformSpace 𝕂⊢ UniformSpace (Matrix m n 𝕂) unfold Matrix𝕂:Type u_1m:Type u_2n:Type u_3inst✝:UniformSpace 𝕂⊢ UniformSpace (m → n → 𝕂); infer_instanceAll goals completed! 🐙

If every term of a series is zero, then its sum is zero.

lemma tsum_eq_zero
    {β : Type*} [TopologicalSpace β] [AddCommMonoid β]
    {f : ℕ → β} (h : ∀ n, f n = 0) :
    (∑' n, f n) = 0 := byβ:Type u_4inst✝¹:TopologicalSpace βinst✝:AddCommMonoid βf:ℕ → βh:∀ (n : ℕ), f n = 0⊢ ∑' (n : ℕ), f n = 0
  simp_all only [tsum_zero]All goals completed! 🐙

The determinant of the matrix exponential

              attribute [local instance] Matrix.linftyOpNormedAlgebraattribute [local instance] Matrix.linftyOpNormedRingattribute [local instance] Matrix.instCompleteSpace

Apply a matrix tsum to a given entry.


lemma matrix_tsum_apply
    {f : ℕ → Matrix m m 𝕂} (hf : Summable f) (i j : m) :
    (∑' n, f n) i j = ∑' n, (f n) i j := by𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:m⊢ (∑' (n : ℕ), f n) i j = ∑' (n : ℕ), f n i j
  have h_row_summable : Summable (fun n ↦ (f n) i) := by
    have h := Pi.summable.1 hf𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:mh:∀ (x : m), Summable fun i => f i x⊢ Summable fun n => f n i𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:mh_row_summable:Summable fun n => f n i⊢ (∑' (n : ℕ), f n) i j = ∑' (n : ℕ), f n i j
    exact h i𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:mh_row_summable:Summable fun n => f n i⊢ (∑' (n : ℕ), f n) i j = ∑' (n : ℕ), f n i j𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:mh_row_summable:Summable fun n => f n i⊢ (∑' (n : ℕ), f n) i j = ∑' (n : ℕ), f n i j
  have h₁ : ((∑' n, f n) : Matrix m m 𝕂) i = (∑' n, (f n) i) := by
    exact tsum_apply hf𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:mh_row_summable:Summable fun n => f n ih₁:(∑' (n : ℕ), f n) i = ∑' (n : ℕ), f n i⊢ (∑' (n : ℕ), f n) i j = ∑' (n : ℕ), f n i j𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:mh_row_summable:Summable fun n => f n ih₁:(∑' (n : ℕ), f n) i = ∑' (n : ℕ), f n i⊢ (∑' (n : ℕ), f n) i j = ∑' (n : ℕ), f n i j
  have h₂ : ((∑' n, (f n) i) : m → 𝕂) j = (∑' n, (f n) i j) := by
    exact tsum_apply h_row_summable𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:mh_row_summable:Summable fun n => f n ih₁:(∑' (n : ℕ), f n) i = ∑' (n : ℕ), f n ih₂:(∑' (n : ℕ), f n i) j = ∑' (n : ℕ), f n i j⊢ (∑' (n : ℕ), f n) i j = ∑' (n : ℕ), f n i j𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:mh_row_summable:Summable fun n => f n ih₁:(∑' (n : ℕ), f n) i = ∑' (n : ℕ), f n ih₂:(∑' (n : ℕ), f n i) j = ∑' (n : ℕ), f n i j⊢ (∑' (n : ℕ), f n) i j = ∑' (n : ℕ), f n i j
  rw [h₁,𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:mh_row_summable:Summable fun n => f n ih₁:(∑' (n : ℕ), f n) i = ∑' (n : ℕ), f n ih₂:(∑' (n : ℕ), f n i) j = ∑' (n : ℕ), f n i j⊢ (∑' (n : ℕ), f n i) j = ∑' (n : ℕ), f n i jAll goals completed! 🐙 h₂𝕂:Type u_1m:Type u_2inst✝:RCLike 𝕂f:ℕ → Matrix m m 𝕂hf:Summable fi:mj:mh_row_summable:Summable fun n => f n ih₁:(∑' (n : ℕ), f n) i = ∑' (n : ℕ), f n ih₂:(∑' (n : ℕ), f n i) j = ∑' (n : ℕ), f n i j⊢ ∑' (n : ℕ), f n i j = ∑' (n : ℕ), f n i jAll goals completed! 🐙]All goals completed! 🐙

For upper-triangular matrices, the diagonal of a product is the product of the diagonals. This is a specific case of a more general property for block-triangular matrices.


lemma diag_mul_of_blockTriangular_id {A B : Matrix m m 𝕂}
    (hA : BlockTriangular A id) (hB : BlockTriangular B id) : (A * B).diag = A.diag * B.diag := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular id⊢ (A * B).diag = A.diag * B.diag
  ext i𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:m⊢ (A * B).diag i = (A.diag * B.diag) i
  simp only [diag_apply, mul_apply, Pi.mul_apply]𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:m⊢ ∑ j, A i j * B j i = A i i * B i i
  apply Finset.sum_eq_single ih₀𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:m⊢ ∀ b ∈ Finset.univ, b ≠ i → A i b * B b i = 0h₁𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:m⊢ i ∉ Finset.univ → A i i * B i i = 0
  ·h₀𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:m⊢ ∀ b ∈ Finset.univ, b ≠ i → A i b * B b i = 0 intro j _ j_ne_ih₀𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:mj:ma✝:j ∈ Finset.univj_ne_i:j ≠ i⊢ A i j * B j i = 0
    cases lt_or_gt_of_ne j_ne_i with
    | inl h =>h₀.inl𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:mj:ma✝:j ∈ Finset.univj_ne_i:j ≠ ih:j < i⊢ A i j * B j i = 0 rw [hA h,h₀.inl𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:mj:ma✝:j ∈ Finset.univj_ne_i:j ≠ ih:j < i⊢ 0 * B j i = 0All goals completed! 🐙 zero_mulh₀.inl𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:mj:ma✝:j ∈ Finset.univj_ne_i:j ≠ ih:j < i⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙 -- j < i
    | inr h =>h₀.inr𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:mj:ma✝:j ∈ Finset.univj_ne_i:j ≠ ih:i < j⊢ A i j * B j i = 0 rw [hB h,h₀.inr𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:mj:ma✝:j ∈ Finset.univj_ne_i:j ≠ ih:i < j⊢ A i j * 0 = 0All goals completed! 🐙 mul_zeroh₀.inr𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:mj:ma✝:j ∈ Finset.univj_ne_i:j ≠ ih:i < j⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙 -- i < j
  ·h₁𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:m⊢ i ∉ Finset.univ → A i i * B i i = 0 introh₁𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂B:Matrix m m 𝕂hA:A.BlockTriangular idhB:B.BlockTriangular idi:ma✝:i ∉ Finset.univ⊢ A i i * B i i = 0; simp_all only [Finset.mem_univ, not_true_eq_false]All goals completed! 🐙

Powers of block triangular matrices are block triangular.


lemma blockTriangular.pow {A : Matrix m m 𝕂} (hA : BlockTriangular A id) (k : ℕ) :
    BlockTriangular (A ^ k) id := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕ⊢ (A ^ k).BlockTriangular id
  induction k with
  | zero =>zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ (A ^ 0).BlockTriangular id rw [pow_zerozero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ BlockTriangular 1 idzero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ BlockTriangular 1 id]zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ BlockTriangular 1 id; exact blockTriangular_oneAll goals completed! 🐙
  | succ k ihk =>succ𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕihk:(A ^ k).BlockTriangular id⊢ (A ^ (k + 1)).BlockTriangular id rw [pow_succsucc𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕihk:(A ^ k).BlockTriangular id⊢ (A ^ k * A).BlockTriangular idsucc𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕihk:(A ^ k).BlockTriangular id⊢ (A ^ k * A).BlockTriangular id]succ𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕihk:(A ^ k).BlockTriangular id⊢ (A ^ k * A).BlockTriangular id; exact ihk.mul hAAll goals completed! 🐙

For an upper-triangular matrix, the diagonal of a power is the power of the diagonal.


lemma diag_pow_of_blockTriangular_id {A : Matrix m m 𝕂}
    (hA : BlockTriangular A id) (k : ℕ) : (A ^ k).diag = A.diag ^ k := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕ⊢ (A ^ k).diag = A.diag ^ k
  induction k with
  | zero =>zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ (A ^ 0).diag = A.diag ^ 0 rw [pow_zero,zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ diag 1 = A.diag ^ 0zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ diag 1 = 1 pow_zerozero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ diag 1 = 1zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ diag 1 = 1]zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ diag 1 = 1; simp [diag_one]All goals completed! 🐙
  | succ k ih =>succ𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕih:(A ^ k).diag = A.diag ^ k⊢ (A ^ (k + 1)).diag = A.diag ^ (k + 1)
    have h_pow_k : BlockTriangular (A ^ k) id := blockTriangular.pow hA ksucc𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕih:(A ^ k).diag = A.diag ^ kh_pow_k:(A ^ k).BlockTriangular id⊢ (A ^ (k + 1)).diag = A.diag ^ (k + 1)
    rw [pow_succ,succ𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕih:(A ^ k).diag = A.diag ^ kh_pow_k:(A ^ k).BlockTriangular id⊢ (A ^ k * A).diag = A.diag ^ (k + 1)All goals completed! 🐙 pow_succ,succ𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕih:(A ^ k).diag = A.diag ^ kh_pow_k:(A ^ k).BlockTriangular id⊢ (A ^ k * A).diag = A.diag ^ k * A.diagAll goals completed! 🐙 diag_mul_of_blockTriangular_id h_pow_k hA,succ𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕih:(A ^ k).diag = A.diag ^ kh_pow_k:(A ^ k).BlockTriangular id⊢ (A ^ k).diag * A.diag = A.diag ^ k * A.diagAll goals completed! 🐙 ihsucc𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idk:ℕih:(A ^ k).diag = A.diag ^ kh_pow_k:(A ^ k).BlockTriangular id⊢ A.diag ^ k * A.diag = A.diag ^ k * A.diagAll goals completed! 🐙]All goals completed! 🐙

The exponential of an upper-triangular matrix is upper-triangular.


lemma blockTriangular_exp_of_blockTriangular_id
    {A : Matrix m m 𝕂} (hA : BlockTriangular A id) :
    (NormedSpace.exp A).BlockTriangular id := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ (NormedSpace.exp A).BlockTriangular id
  intro i j hij𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id i⊢ NormedSpace.exp A i j = 0
  rw [NormedSpace.exp_eq_tsum 𝕂𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id i⊢ (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) A i j = 0𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id i⊢ (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) A i j = 0]𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id i⊢ (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) A i j = 0
  let exp_series := fun n => ((n.factorial : 𝕂)⁻¹) • (A ^ n)𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ n⊢ (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) A i j = 0
  change (∑' n, exp_series n) i j = 0𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ n⊢ (∑' (n : ℕ), exp_series n) i j = 0
  rw [matrix_tsum_apply (NormedSpace.expSeries_summable' A) i j𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ n⊢ ∑' (n : ℕ), ((↑n.factorial)⁻¹ • A ^ n) i j = 0𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ n⊢ ∑' (n : ℕ), ((↑n.factorial)⁻¹ • A ^ n) i j = 0]𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ n⊢ ∑' (n : ℕ), ((↑n.factorial)⁻¹ • A ^ n) i j = 0
  apply tsum_eq_zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ n⊢ ∀ (n : ℕ), ((↑n.factorial)⁻¹ • A ^ n) i j = 0
  intro n𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕ⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0
  have h_pow : BlockTriangular (A ^ n) id := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ (NormedSpace.exp A).BlockTriangular id𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0
    induction n with
    | zero =>zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ n⊢ (A ^ 0).BlockTriangular id𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0 rw [pow_zerozero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ n⊢ BlockTriangular 1 idzero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ n⊢ BlockTriangular 1 id𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0]zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ n⊢ BlockTriangular 1 id𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0; exact blockTriangular_oneAll goals completed! 🐙𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0
    | succ k ihk =>succ𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nk:ℕihk:(A ^ k).BlockTriangular id⊢ (A ^ (k + 1)).BlockTriangular id𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0 rw [pow_succsucc𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nk:ℕihk:(A ^ k).BlockTriangular id⊢ (A ^ k * A).BlockTriangular idsucc𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nk:ℕihk:(A ^ k).BlockTriangular id⊢ (A ^ k * A).BlockTriangular id𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0]succ𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nk:ℕihk:(A ^ k).BlockTriangular id⊢ (A ^ k * A).BlockTriangular id𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0; exact ihk.mul hA𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ ((↑n.factorial)⁻¹ • A ^ n) i j = 0
  simp only [smul_apply]𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ (↑n.factorial)⁻¹ • (A ^ n) i j = 0
  rw [h_pow hij,𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ (↑n.factorial)⁻¹ • 0 = 0All goals completed! 🐙 smul_zero𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:mj:mhij:id j < id iexp_series:ℕ → Matrix m m 𝕂 := fun n => (↑n.factorial)⁻¹ • A ^ nn:ℕh_pow:(A ^ n).BlockTriangular id⊢ 0 = 0All goals completed! 🐙]All goals completed! 🐙

For an upper–triangular matrix A, the (i,i) entry of the power A ^ n is simply the n-th power of the original diagonal entry.

lemma diag_pow_entry_eq_pow_diag_entry {A : Matrix m m 𝕂}
    (hA : BlockTriangular A id) (n : ℕ) (i : m) :
    (A ^ n) i i = (A i i) ^ n := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idn:ℕi:m⊢ (A ^ n) i i = A i i ^ n
  have h := diag_pow_of_blockTriangular_id hA n𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idn:ℕi:mh:(A ^ n).diag = A.diag ^ n⊢ (A ^ n) i i = A i i ^ n
  simpa [diag_apply, Pi.pow_apply] using congr_arg (fun d => d i) hAll goals completed! 🐙

Each term in the matrix exponential series equals the corresponding scalar term on the diagonal

lemma exp_series_diag_term_eq {A : Matrix m m 𝕂} (hA : BlockTriangular A id)
    (n : ℕ) (i : m) :
    ((n.factorial : 𝕂)⁻¹ • (A ^ n)) i i = (n.factorial : 𝕂)⁻¹ • (A i i) ^ n := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idn:ℕi:m⊢ ((↑n.factorial)⁻¹ • A ^ n) i i = (↑n.factorial)⁻¹ • A i i ^ n
  simp [smul_apply, diag_pow_entry_eq_pow_diag_entry hA]All goals completed! 🐙

The diagonal of the matrix exponential series equals the scalar exponential series

lemma matrix_exp_series_diag_eq_scalar_series {A : Matrix m m 𝕂} (hA : BlockTriangular A id)
    (i : m) :
    (∑' n, ((n.factorial : 𝕂)⁻¹ • (A ^ n)) i i) = ∑' n, (n.factorial : 𝕂)⁻¹ • (A i i) ^ n := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ ∑' (n : ℕ), ((↑n.factorial)⁻¹ • A ^ n) i i = ∑' (n : ℕ), (↑n.factorial)⁻¹ • A i i ^ n
  exact tsum_congr (exp_series_diag_term_eq hA · i)All goals completed! 🐙

The diagonal of the exponential of an upper-triangular matrix A consists of the exponentials of the diagonal entries of A.


theorem diag_exp_of_blockTriangular_id
    {A : Matrix m m 𝕂} (hA : BlockTriangular A id) :
    (NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i) := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ (NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i)
  funext i𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ (NormedSpace.exp A).diag i = NormedSpace.exp (A i i)
  rw [NormedSpace.exp_eq_tsum 𝕂,𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ ((fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) A).diag i = NormedSpace.exp (A i i)𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) A i i = NormedSpace.exp (A i i) diag_apply𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) A i i = NormedSpace.exp (A i i)𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) A i i = NormedSpace.exp (A i i)]𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) A i i = NormedSpace.exp (A i i)
  simp_rw [𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ (∑' (n : ℕ), (↑n.factorial)⁻¹ • A ^ n) i i = NormedSpace.exp (A i i)matrix_tsum_apply (NormedSpace.expSeries_summable' A) i i𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ ∑' (n : ℕ), ((↑n.factorial)⁻¹ • A ^ n) i i = NormedSpace.exp (A i i)]
  rw [matrix_exp_series_diag_eq_scalar_series hA i𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • A i i ^ n = NormedSpace.exp (A i i)𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • A i i ^ n = NormedSpace.exp (A i i)]𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • A i i ^ n = NormedSpace.exp (A i i)
  rw [NormedSpace.exp_eq_tsum 𝕂𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idi:m⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • A i i ^ n = (fun x => ∑' (n : ℕ), (↑n.factorial)⁻¹ • x ^ n) (A i i)All goals completed! 🐙]All goals completed! 🐙

Lie's trace formula for upper triangular matrices.


lemma det_exp_of_blockTriangular_id {A : Matrix m m 𝕂} (hA : BlockTriangular A id) :
    (NormedSpace.exp A).det = NormedSpace.exp A.trace := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular id⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace
  have h_exp_upper : BlockTriangular (NormedSpace.exp A) id :=
    blockTriangular_exp_of_blockTriangular_id hA𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular id⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace
  rw [det_of_upperTriangular h_exp_upper𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular id⊢ ∏ i, NormedSpace.exp A i i = NormedSpace.exp A.trace𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular id⊢ ∏ i, NormedSpace.exp A i i = NormedSpace.exp A.trace]𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular id⊢ ∏ i, NormedSpace.exp A i i = NormedSpace.exp A.trace
  have h_diag_exp : (NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i) :=
    diag_exp_of_blockTriangular_id hA𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular idh_diag_exp:(NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i)⊢ ∏ i, NormedSpace.exp A i i = NormedSpace.exp A.trace
  simp_rw [𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular idh_diag_exp:(NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i)⊢ ∏ i, NormedSpace.exp A i i = NormedSpace.exp A.trace← diag_apply𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular idh_diag_exp:(NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i)⊢ ∏ x, (NormedSpace.exp A).diag x = NormedSpace.exp A.trace]
  simp_rw [𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular idh_diag_exp:(NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i)⊢ ∏ x, (NormedSpace.exp A).diag x = NormedSpace.exp A.traceh_diag_exp𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular idh_diag_exp:(NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i)⊢ ∏ x, NormedSpace.exp (A x x) = NormedSpace.exp A.trace]
  rw [← NormedSpace.exp_sum Finset.univ𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular idh_diag_exp:(NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i)⊢ NormedSpace.exp (∑ i, A i i) = NormedSpace.exp A.trace𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular idh_diag_exp:(NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i)⊢ NormedSpace.exp (∑ i, A i i) = NormedSpace.exp A.trace]𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂hA:A.BlockTriangular idh_exp_upper:(NormedSpace.exp A).BlockTriangular idh_diag_exp:(NormedSpace.exp A).diag = fun i => NormedSpace.exp (A i i)⊢ NormedSpace.exp (∑ i, A i i) = NormedSpace.exp A.trace
  congr 1All goals completed! 🐙

The trace is invariant under unitary conjugation.

lemma trace_unitary_conj (A : Matrix m m 𝕂) (U : unitaryGroup m 𝕂) :
    trace ((U : Matrix m m 𝕂) * A * star (U : Matrix m m 𝕂)) = trace A := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ (↑U * A * star ↑U).trace = A.trace
  have h_unitary : star (U : Matrix m m 𝕂) * (U : Matrix m m 𝕂) = 1 :=
    UnitaryGroup.star_mul_self U𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)h_unitary:star ↑U * ↑U = 1⊢ (↑U * A * star ↑U).trace = A.trace
  simpa [Matrix.mul_assoc, h_unitary, Matrix.one_mul] using
    (Matrix.trace_mul_cycle (U : Matrix m m 𝕂) A (star (U : Matrix m m 𝕂)))All goals completed! 🐙

The determinant is invariant under unitary conjugation.


lemma det_unitary_conj (A : Matrix m m 𝕂) (U : unitaryGroup m 𝕂) :
    det ((U : Matrix m m 𝕂) * A * star (U : Matrix m m 𝕂)) = det A := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ (↑U * A * star ↑U).det = A.det
  rw [det_mul_right_comm𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ (↑U * star ↑U * A).det = A.det𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ (↑U * star ↑U * A).det = A.det]𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ (↑U * star ↑U * A).det = A.det
  simp_all only [SetLike.coe_mem, Unitary.mul_star_self_of_mem, one_mul]All goals completed! 🐙

The exponential of a matrix commutes with unitary conjugation.


lemma exp_unitary_conj (A : Matrix m m 𝕂) (U : unitaryGroup m 𝕂) :
    NormedSpace.exp ((U : Matrix m m 𝕂) * A * star (U : Matrix m m 𝕂)) =
      (U : Matrix m m 𝕂) * NormedSpace.exp A * star (U : Matrix m m 𝕂) := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ NormedSpace.exp (↑U * A * star ↑U) = ↑U * NormedSpace.exp A * star ↑U
  let Uu : (Matrix m m 𝕂)ˣ :=
    { val := (U : Matrix m m 𝕂)
      inv := star (U : Matrix m m 𝕂)
      val_inv := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ ↑U * star ↑U = 1𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)Uu:(Matrix m m 𝕂)ˣ := { val := ↑U, inv := star ↑U, val_inv := ⋯, inv_val := ⋯ }⊢ NormedSpace.exp (↑U * A * star ↑U) = ↑U * NormedSpace.exp A * star ↑U simpAll goals completed! 🐙𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)Uu:(Matrix m m 𝕂)ˣ := { val := ↑U, inv := star ↑U, val_inv := ⋯, inv_val := ⋯ }⊢ NormedSpace.exp (↑U * A * star ↑U) = ↑U * NormedSpace.exp A * star ↑U
      inv_val := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ star ↑U * ↑U = 1𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)Uu:(Matrix m m 𝕂)ˣ := { val := ↑U, inv := star ↑U, val_inv := ⋯, inv_val := ⋯ }⊢ NormedSpace.exp (↑U * A * star ↑U) = ↑U * NormedSpace.exp A * star ↑U simpAll goals completed! 🐙𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)Uu:(Matrix m m 𝕂)ˣ := { val := ↑U, inv := star ↑U, val_inv := ⋯, inv_val := ⋯ }⊢ NormedSpace.exp (↑U * A * star ↑U) = ↑U * NormedSpace.exp A * star ↑U}𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)Uu:(Matrix m m 𝕂)ˣ := { val := ↑U, inv := star ↑U, val_inv := ⋯, inv_val := ⋯ }⊢ NormedSpace.exp (↑U * A * star ↑U) = ↑U * NormedSpace.exp A * star ↑U
  have h_units := Matrix.exp_units_conj Uu A𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)Uu:(Matrix m m 𝕂)ˣ := { val := ↑U, inv := star ↑U, val_inv := ⋯, inv_val := ⋯ }h_units:NormedSpace.exp (↑Uu * A * ↑Uu⁻¹) = ↑Uu * NormedSpace.exp A * ↑Uu⁻¹⊢ NormedSpace.exp (↑U * A * star ↑U) = ↑U * NormedSpace.exp A * star ↑U
  simpa [Uu] using h_unitsAll goals completed! 🐙



lemma det_exp_unitary_conj (A : Matrix m m 𝕂) (U : unitaryGroup m 𝕂) :
    (NormedSpace.exp ((U : Matrix m m 𝕂) * A * star (U : Matrix m m 𝕂))).det =
    (NormedSpace.exp A).det := by𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ (NormedSpace.exp (↑U * A * star ↑U)).det = (NormedSpace.exp A).det
  rw [exp_unitary_conj,𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ (↑U * NormedSpace.exp A * star ↑U).det = (NormedSpace.exp A).detAll goals completed! 🐙 det_unitary_conj𝕂:Type u_1m:Type u_2inst✝²:RCLike 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂)⊢ (NormedSpace.exp A).det = (NormedSpace.exp A).detAll goals completed! 🐙]All goals completed! 🐙

The determinant of the exponential of a matrix is the exponential of its trace. This is also known as Lie's trace formula.


theorem det_exp {𝕂 m : Type*} [RCLike 𝕂] [IsAlgClosed 𝕂] [Fintype m] [LinearOrder m]
    (A : Matrix m m 𝕂) :
    (NormedSpace.exp A).det = NormedSpace.exp A.trace := by𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace
  let U := A.schurTriangulationUnitary𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitary⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace
  let T := A.schurTriangulation𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulation⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace
  have h_prop : T.val.IsUpperTriangular := T.property𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangular⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace
  have h_conj : A = U * T * star U := schur_triangulation A𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace
  have h_trace_invariant : A.trace = T.val.trace := by
    rw [h_conj,𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)⊢ (↑U * ↑T * ↑(star U)).trace = (↑T).trace𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).trace⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace Unitary.coe_star,𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)⊢ (↑U * ↑T * star ↑U).trace = (↑T).trace𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).trace⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace trace_unitary_conj𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)⊢ (↑T).trace = (↑T).trace𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).trace⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace]𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).trace⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).trace⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace
  have h_det_invariant : (NormedSpace.exp A).det = (NormedSpace.exp T.val).det := by
    rw [h_conj,𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).trace⊢ (NormedSpace.exp (↑U * ↑T * ↑(star U))).det = (NormedSpace.exp ↑T).det𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).traceh_det_invariant:(NormedSpace.exp A).det = (NormedSpace.exp ↑T).det⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace Unitary.coe_star,𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).trace⊢ (NormedSpace.exp (↑U * ↑T * star ↑U)).det = (NormedSpace.exp ↑T).det𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).traceh_det_invariant:(NormedSpace.exp A).det = (NormedSpace.exp ↑T).det⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace det_exp_unitary_conj𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).trace⊢ (NormedSpace.exp ↑T).det = (NormedSpace.exp ↑T).det𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).traceh_det_invariant:(NormedSpace.exp A).det = (NormedSpace.exp ↑T).det⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace]𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).traceh_det_invariant:(NormedSpace.exp A).det = (NormedSpace.exp ↑T).det⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).traceh_det_invariant:(NormedSpace.exp A).det = (NormedSpace.exp ↑T).det⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace
  have h_triangular_case : (NormedSpace.exp T.val).det = NormedSpace.exp T.val.trace :=
    det_exp_of_blockTriangular_id h_prop𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).traceh_det_invariant:(NormedSpace.exp A).det = (NormedSpace.exp ↑T).deth_triangular_case:(NormedSpace.exp ↑T).det = NormedSpace.exp (↑T).trace⊢ (NormedSpace.exp A).det = NormedSpace.exp A.trace
  rw [h_det_invariant,𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).traceh_det_invariant:(NormedSpace.exp A).det = (NormedSpace.exp ↑T).deth_triangular_case:(NormedSpace.exp ↑T).det = NormedSpace.exp (↑T).trace⊢ (NormedSpace.exp ↑T).det = NormedSpace.exp A.traceAll goals completed! 🐙 h_triangular_case,𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).traceh_det_invariant:(NormedSpace.exp A).det = (NormedSpace.exp ↑T).deth_triangular_case:(NormedSpace.exp ↑T).det = NormedSpace.exp (↑T).trace⊢ NormedSpace.exp (↑T).trace = NormedSpace.exp A.traceAll goals completed! 🐙 h_trace_invariant𝕂:Type u_4m:Type u_5inst✝³:RCLike 𝕂inst✝²:IsAlgClosed 𝕂inst✝¹:Fintype minst✝:LinearOrder mA:Matrix m m 𝕂U:↥(unitaryGroup m 𝕂) := A.schurTriangulationUnitaryT:UpperTriangular m 𝕂 := A.schurTriangulationh_prop:(↑T).IsUpperTriangularh_conj:A = ↑U * ↑T * ↑(star U)h_trace_invariant:A.trace = (↑T).traceh_det_invariant:(NormedSpace.exp A).det = (NormedSpace.exp ↑T).deth_triangular_case:(NormedSpace.exp ↑T).det = NormedSpace.exp (↑T).trace⊢ NormedSpace.exp (↑T).trace = NormedSpace.exp (↑T).traceAll goals completed! 🐙]All goals completed! 🐙

              -- `Matrix.map` commutes with an absolutely convergent series.
lemma map_tsum {α β m n : Type*}
    [AddCommMonoid α] [AddCommMonoid β] [TopologicalSpace α] [TopologicalSpace β]
    [T2Space β]
    (f : α →+ β) (hf : Continuous f) {s : ℕ → Matrix m n α} (hs : Summable s) :
    (∑' k, s k).map f = ∑' k, (s k).map f := byα:Type u_4β:Type u_5m:Type u_6n:Type u_7inst✝⁴:AddCommMonoid αinst✝³:AddCommMonoid βinst✝²:TopologicalSpace αinst✝¹:TopologicalSpace βinst✝:T2Space βf:α →+ βhf:Continuous[inst✝², inst✝¹] ⇑fs:ℕ → Matrix m n αhs:Summable s⊢ (∑' (k : ℕ), s k).map ⇑f = ∑' (k : ℕ), (s k).map ⇑f
  let F : Matrix m n α →+ Matrix m n β := AddMonoidHom.mapMatrix fα:Type u_4β:Type u_5m:Type u_6n:Type u_7inst✝⁴:AddCommMonoid αinst✝³:AddCommMonoid βinst✝²:TopologicalSpace αinst✝¹:TopologicalSpace βinst✝:T2Space βf:α →+ βhf:Continuous[inst✝², inst✝¹] ⇑fs:ℕ → Matrix m n αhs:Summable sF:Matrix m n α →+ Matrix m n β := f.mapMatrix⊢ (∑' (k : ℕ), s k).map ⇑f = ∑' (k : ℕ), (s k).map ⇑f
  have hF : Continuous F := Continuous.matrix_map continuous_id hfα:Type u_4β:Type u_5m:Type u_6n:Type u_7inst✝⁴:AddCommMonoid αinst✝³:AddCommMonoid βinst✝²:TopologicalSpace αinst✝¹:TopologicalSpace βinst✝:T2Space βf:α →+ βhf:Continuous[inst✝², inst✝¹] ⇑fs:ℕ → Matrix m n αhs:Summable sF:Matrix m n α →+ Matrix m n β := f.mapMatrixhF:Continuous[instTopologicalSpaceMatrix, instTopologicalSpaceMatrix] ⇑F⊢ (∑' (k : ℕ), s k).map ⇑f = ∑' (k : ℕ), (s k).map ⇑f
  exact (hs.hasSum.map F hF).tsum_eq.symmAll goals completed! 🐙attribute [local instance] Matrix.linftyOpNormedAlgebraattribute [local instance] Matrix.linftyOpNormedRingattribute [local instance] Matrix.instCompleteSpace

set_option backward.isDefEq.respectTransparency false in
lemma exp_map_algebraMap {n : Type*} [Fintype n] [DecidableEq n]
    (A : Matrix n n ℝ) :
    (exp A).map (algebraMap ℝ ℂ) = exp (A.map (algebraMap ℝ ℂ)) := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝ⊢ (exp A).map ⇑(algebraMap ℝ ℂ) = exp (A.map ⇑(algebraMap ℝ ℂ))
  letI : SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRing⊢ (exp A).map ⇑(algebraMap ℝ ℂ) = exp (A.map ⇑(algebraMap ℝ ℂ))
  letI : NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRing⊢ (exp A).map ⇑(algebraMap ℝ ℂ) = exp (A.map ⇑(algebraMap ℝ ℂ))
  letI : NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebran:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝¹:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebra⊢ (exp A).map ⇑(algebraMap ℝ ℂ) = exp (A.map ⇑(algebraMap ℝ ℂ))
  letI : CompleteSpace (Matrix n n ℝ) := inferInstancen:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝²:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℝ) := ···⊢ (exp A).map ⇑(algebraMap ℝ ℂ) = exp (A.map ⇑(algebraMap ℝ ℂ))
  letI : SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝³:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝²:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝¹:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝:CompleteSpace (Matrix n n ℝ) := ···this:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRing⊢ (exp A).map ⇑(algebraMap ℝ ℂ) = exp (A.map ⇑(algebraMap ℝ ℂ))
  letI : NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁴:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝³:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝²:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝¹:CompleteSpace (Matrix n n ℝ) := ···this✝:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRing⊢ (exp A).map ⇑(algebraMap ℝ ℂ) = exp (A.map ⇑(algebraMap ℝ ℂ))
  letI : NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebran:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁵:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁴:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝³:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝²:CompleteSpace (Matrix n n ℝ) := ···this✝¹:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebra⊢ (exp A).map ⇑(algebraMap ℝ ℂ) = exp (A.map ⇑(algebraMap ℝ ℂ))
  letI : CompleteSpace (Matrix n n ℂ) := inferInstancen:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···⊢ (exp A).map ⇑(algebraMap ℝ ℂ) = exp (A.map ⇑(algebraMap ℝ ℂ))
  simp only [exp_eq_tsum ℝ]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···⊢ (∑' (n_1 : ℕ), (↑n_1.factorial)⁻¹ • A ^ n_1).map ⇑(algebraMap ℝ ℂ) =
  ∑' (n_1 : ℕ), (↑n_1.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ n_1
  have hs : Summable (fun k => (k.factorial : ℝ)⁻¹ • A ^ k) := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝ⊢ (exp A).map ⇑(algebraMap ℝ ℂ) = exp (A.map ⇑(algebraMap ℝ ℂ))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ k⊢ (∑' (n_1 : ℕ), (↑n_1.factorial)⁻¹ • A ^ n_1).map ⇑(algebraMap ℝ ℂ) =
  ∑' (n_1 : ℕ), (↑n_1.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ n_1
    exact NormedSpace.expSeries_summable' An:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ k⊢ (∑' (n_1 : ℕ), (↑n_1.factorial)⁻¹ • A ^ n_1).map ⇑(algebraMap ℝ ℂ) =
  ∑' (n_1 : ℕ), (↑n_1.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ n_1n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ k⊢ (∑' (n_1 : ℕ), (↑n_1.factorial)⁻¹ • A ^ n_1).map ⇑(algebraMap ℝ ℂ) =
  ∑' (n_1 : ℕ), (↑n_1.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ n_1
  erw [Matrix.map_tsum (algebraMap ℝ ℂ).toAddMonoidHom RCLike.continuous_ofReal hsn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ k⊢ ∑' (k : ℕ), ((↑k.factorial)⁻¹ • A ^ k).map ⇑(algebraMap ℝ ℂ).toAddMonoidHom =
  ∑' (n_1 : ℕ), (↑n_1.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ n_1]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ k⊢ ∑' (k : ℕ), ((↑k.factorial)⁻¹ • A ^ k).map ⇑(algebraMap ℝ ℂ).toAddMonoidHom =
  ∑' (n_1 : ℕ), (↑n_1.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ n_1
  apply tsum_congrn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ k⊢ ∀ (b : ℕ),
  ((↑b.factorial)⁻¹ • A ^ b).map ⇑(algebraMap ℝ ℂ).toAddMonoidHom = (↑b.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ b
  intro kn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ kk:ℕ⊢ ((↑k.factorial)⁻¹ • A ^ k).map ⇑(algebraMap ℝ ℂ).toAddMonoidHom = (↑k.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ k
  erw [Matrix.map_smul,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ kk:ℕ⊢ (↑k.factorial)⁻¹ • (A ^ k).map ⇑(algebraMap ℝ ℂ).toAddMonoidHom = (↑k.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ khfn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ kk:ℕ⊢ ∀ (a : ℝ), (algebraMap ℝ ℂ).toAddMonoidHom ((↑k.factorial)⁻¹ • a) = (↑k.factorial)⁻¹ • (algebraMap ℝ ℂ).toAddMonoidHom a Matrix.map_pow A (algebraMap ℝ ℂ) kn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ kk:ℕ⊢ (↑k.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ k = (↑k.factorial)⁻¹ • A.map ⇑(algebraMap ℝ ℂ) ^ khfn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ kk:ℕ⊢ ∀ (a : ℝ), (algebraMap ℝ ℂ).toAddMonoidHom ((↑k.factorial)⁻¹ • a) = (↑k.factorial)⁻¹ • (algebraMap ℝ ℂ).toAddMonoidHom a]hfn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nA:Matrix n n ℝthis✝⁶:SeminormedRing (Matrix n n ℝ) := Matrix.linftyOpSemiNormedRingthis✝⁵:NormedRing (Matrix n n ℝ) := Matrix.linftyOpNormedRingthis✝⁴:NormedAlgebra ℝ (Matrix n n ℝ) := Matrix.linftyOpNormedAlgebrathis✝³:CompleteSpace (Matrix n n ℝ) := ···this✝²:SeminormedRing (Matrix n n ℂ) := Matrix.linftyOpSemiNormedRingthis✝¹:NormedRing (Matrix n n ℂ) := Matrix.linftyOpNormedRingthis✝:NormedAlgebra ℂ (Matrix n n ℂ) := Matrix.linftyOpNormedAlgebrathis:CompleteSpace (Matrix n n ℂ) := ···hs:Summable fun k => (↑k.factorial)⁻¹ • A ^ kk:ℕ⊢ ∀ (a : ℝ), (algebraMap ℝ ℂ).toAddMonoidHom ((↑k.factorial)⁻¹ • a) = (↑k.factorial)⁻¹ • (algebraMap ℝ ℂ).toAddMonoidHom a
  simpAll goals completed! 🐙

Lie's trace formula over ℝ: det(exp(A)) = exp(tr(A)) for any real matrix A. This is proved by transferring the result from ℂ using the naturality of polynomial identities.


theorem det_exp_real {n : Type*} [Fintype n] [LinearOrder n]
    (A : Matrix n n ℝ) : (NormedSpace.exp A).det = Real.exp A.trace := byn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝ⊢ (NormedSpace.exp A).det = Real.exp A.trace
  let A_ℂ := A.map (algebraMap ℝ ℂ)n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)⊢ (NormedSpace.exp A).det = Real.exp A.trace
  have h_complex : (NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.trace := by
    haveI : IsAlgClosed ℂ := Complex.isAlgClosedn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)this:IsAlgClosed ℂ⊢ (NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.tracen:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.trace⊢ (NormedSpace.exp A).det = Real.exp A.trace
    rw [Complex.exp_eq_exp_ℂ,n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)this:IsAlgClosed ℂ⊢ (NormedSpace.exp A_ℂ).det = NormedSpace.exp A_ℂ.tracen:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.trace⊢ (NormedSpace.exp A).det = Real.exp A.trace ← Matrix.det_expn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)this:IsAlgClosed ℂ⊢ (NormedSpace.exp A_ℂ).det = (NormedSpace.exp A_ℂ).detn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.trace⊢ (NormedSpace.exp A).det = Real.exp A.trace]n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.trace⊢ (NormedSpace.exp A).det = Real.exp A.tracen:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.trace⊢ (NormedSpace.exp A).det = Real.exp A.trace
  have h_trace_comm : A_ℂ.trace = (algebraMap ℝ ℂ) A.trace := by
    simp only [A_ℂ, trace, diag_map, map_sum]n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.trace⊢ ∑ x, (⇑(algebraMap ℝ ℂ) ∘ A.diag) x = ∑ x, (algebraMap ℝ ℂ) (A.diag x)n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.trace⊢ (NormedSpace.exp A).det = Real.exp A.trace;rfln:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.trace⊢ (NormedSpace.exp A).det = Real.exp A.tracen:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.trace⊢ (NormedSpace.exp A).det = Real.exp A.trace
  have h_det_comm : (algebraMap ℝ ℂ) ((NormedSpace.exp A).det) = (NormedSpace.exp A_ℂ).det := by
    rw [@RingHom.map_detn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.trace⊢ ((algebraMap ℝ ℂ).mapMatrix (NormedSpace.exp A)).det = (NormedSpace.exp A_ℂ).detn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.trace⊢ ((algebraMap ℝ ℂ).mapMatrix (NormedSpace.exp A)).det = (NormedSpace.exp A_ℂ).detn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.trace]n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.trace⊢ ((algebraMap ℝ ℂ).mapMatrix (NormedSpace.exp A)).det = (NormedSpace.exp A_ℂ).detn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.trace
    rw [← NormedSpace.exp_map_algebraMapn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.trace⊢ ((algebraMap ℝ ℂ).mapMatrix (NormedSpace.exp A)).det = ((NormedSpace.exp A).map ⇑(algebraMap ℝ ℂ)).detn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.trace⊢ ((algebraMap ℝ ℂ).mapMatrix (NormedSpace.exp A)).det = ((NormedSpace.exp A).map ⇑(algebraMap ℝ ℂ)).detn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.trace]n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.trace⊢ ((algebraMap ℝ ℂ).mapMatrix (NormedSpace.exp A)).det = ((NormedSpace.exp A).map ⇑(algebraMap ℝ ℂ)).detn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.trace; rfln:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.tracen:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(NormedSpace.exp A_ℂ).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.trace
  rw [← h_det_commn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.tracen:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.trace] at h_complexn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp A_ℂ.traceh_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.trace
  rw [h_trace_commn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp ((algebraMap ℝ ℂ) A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.tracen:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp ((algebraMap ℝ ℂ) A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.trace] at h_complexn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp ((algebraMap ℝ ℂ) A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ (NormedSpace.exp A).det = Real.exp A.trace
  have h_exp_comm : Complex.exp ((algebraMap ℝ ℂ) A.trace) =
      (algebraMap ℝ ℂ) (Real.exp A.trace) := by
    rw [Complex.coe_algebraMap,n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp ((algebraMap ℝ ℂ) A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ Complex.exp ↑A.trace = ↑(Real.exp A.trace)n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp ((algebraMap ℝ ℂ) A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).deth_exp_comm:Complex.exp ((algebraMap ℝ ℂ) A.trace) = (algebraMap ℝ ℂ) (Real.exp A.trace)⊢ (NormedSpace.exp A).det = Real.exp A.trace ← Complex.ofReal_expn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp ((algebraMap ℝ ℂ) A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).det⊢ ↑(Real.exp A.trace) = ↑(Real.exp A.trace)n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp ((algebraMap ℝ ℂ) A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).deth_exp_comm:Complex.exp ((algebraMap ℝ ℂ) A.trace) = (algebraMap ℝ ℂ) (Real.exp A.trace)⊢ (NormedSpace.exp A).det = Real.exp A.trace]n:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp ((algebraMap ℝ ℂ) A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).deth_exp_comm:Complex.exp ((algebraMap ℝ ℂ) A.trace) = (algebraMap ℝ ℂ) (Real.exp A.trace)⊢ (NormedSpace.exp A).det = Real.exp A.tracen:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = Complex.exp ((algebraMap ℝ ℂ) A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).deth_exp_comm:Complex.exp ((algebraMap ℝ ℂ) A.trace) = (algebraMap ℝ ℂ) (Real.exp A.trace)⊢ (NormedSpace.exp A).det = Real.exp A.trace
  rw [h_exp_commn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (algebraMap ℝ ℂ) (Real.exp A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).deth_exp_comm:Complex.exp ((algebraMap ℝ ℂ) A.trace) = (algebraMap ℝ ℂ) (Real.exp A.trace)⊢ (NormedSpace.exp A).det = Real.exp A.tracen:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (algebraMap ℝ ℂ) (Real.exp A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).deth_exp_comm:Complex.exp ((algebraMap ℝ ℂ) A.trace) = (algebraMap ℝ ℂ) (Real.exp A.trace)⊢ (NormedSpace.exp A).det = Real.exp A.trace] at h_complexn:Type u_1inst✝¹:Fintype ninst✝:LinearOrder nA:Matrix n n ℝA_ℂ:Matrix n n ℂ := A.map ⇑(algebraMap ℝ ℂ)h_complex:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (algebraMap ℝ ℂ) (Real.exp A.trace)h_trace_comm:A_ℂ.trace = (algebraMap ℝ ℂ) A.traceh_det_comm:(algebraMap ℝ ℂ) (NormedSpace.exp A).det = (NormedSpace.exp A_ℂ).deth_exp_comm:Complex.exp ((algebraMap ℝ ℂ) A.trace) = (algebraMap ℝ ℂ) (Real.exp A.trace)⊢ (NormedSpace.exp A).det = Real.exp A.trace
  exact Complex.ofReal_injective h_complexAll goals completed! 🐙