-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_neg (A : Matrix m m 𝔸) : exp 𝕂 (-A) = (exp 𝕂 A)⁻¹

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
⊢ exp 𝕂 (-A) = (exp 𝕂 A)⁻¹

Tactic:
rw [nonsing_inv_eq_ring_inverse]

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
⊢ exp 𝕂 (-A) = Ring.inverse (exp 𝕂 A)

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this✝ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
⊢ exp 𝕂 (-A) = Ring.inverse (exp 𝕂 A)

Tactic:
letI : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra
⊢ exp 𝕂 (-A) = Ring.inverse (exp 𝕂 A)

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
⊢ exp 𝕂 (-A) = Ring.inverse (exp 𝕂 A)

Tactic:
letI : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this✝ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
⊢ exp 𝕂 (-A) = Ring.inverse (exp 𝕂 A)

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing
this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra
⊢ exp 𝕂 (-A) = Ring.inverse (exp 𝕂 A)

Tactic:
exact (Ring.inverse_exp _ A).symm

Result:
no goals

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
⊢ exp 𝕂 (-A) = Ring.inverse (exp 𝕂 A)

Tactic:
letI : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing

Result:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
this : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing
⊢ exp 𝕂 (-A) = Ring.inverse (exp 𝕂 A)