Skip to content

Commit 1c10ceb

Browse files
YaelDilliesYaelDillies
committed
chore(LinearAlgebra/Matrix): import less analysis (#31518)
Follow up to #31480. Also fix a few namespacing issues that arose.
1 parent 0939636 commit 1c10ceb

File tree

9 files changed

+118
-108
lines changed

9 files changed

+118
-108
lines changed

β€ŽMathlib.leanβ€Ž

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1814,7 +1814,9 @@ import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
18141814
import Mathlib.Analysis.LocallyConvex.WeakSpace
18151815
import Mathlib.Analysis.LocallyConvex.WithSeminorms
18161816
import Mathlib.Analysis.Matrix
1817+
import Mathlib.Analysis.Matrix.Hermitian
18171818
import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
1819+
import Mathlib.Analysis.Matrix.LDL
18181820
import Mathlib.Analysis.Matrix.Normed
18191821
import Mathlib.Analysis.Matrix.Order
18201822
import Mathlib.Analysis.Matrix.PosDef
@@ -4473,7 +4475,6 @@ import Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
44734475
import Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
44744476
import Mathlib.LinearAlgebra.Matrix.IsDiag
44754477
import Mathlib.LinearAlgebra.Matrix.Kronecker
4476-
import Mathlib.LinearAlgebra.Matrix.LDL
44774478
import Mathlib.LinearAlgebra.Matrix.MvPolynomial
44784479
import Mathlib.LinearAlgebra.Matrix.Nondegenerate
44794480
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse

β€ŽMathlib/Analysis/InnerProductSpace/GramMatrix.leanβ€Ž

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2025 Peter Pfaffelhuber. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Peter Pfaffelhuber
55
-/
6-
6+
import Mathlib.Analysis.InnerProductSpace.Basic
77
import Mathlib.LinearAlgebra.Matrix.PosDef
88

99
/-! # Gram Matrices

β€ŽMathlib/Analysis/InnerProductSpace/Positive.leanβ€Ž

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Anatole Dedecker
55
-/
66
import Mathlib.Analysis.InnerProductSpace.Spectrum
7+
import Mathlib.Analysis.Matrix.Hermitian
78
import Mathlib.LinearAlgebra.Matrix.PosDef
89

910
/-!

β€ŽMathlib/Analysis/Matrix/Hermitian.leanβ€Ž

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
/-
2+
Copyright (c) 2022 Alexander Bentkamp. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Alexander Bentkamp
5+
-/
6+
import Mathlib.Analysis.InnerProductSpace.PiL2
7+
import Mathlib.LinearAlgebra.Matrix.Hermitian
8+
9+
/-!
10+
# Hermitian matrices over ℝ and β„‚
11+
12+
This file proves that Hermitian matrices over ℝ and β„‚ are exactly the ones whose corresponding
13+
linear map is self-adjoint.
14+
15+
## Tags
16+
17+
self-adjoint matrix, hermitian matrix
18+
-/
19+
20+
-- TODO:
21+
-- assert_not_exists MonoidAlgebra
22+
23+
open RCLike
24+
25+
namespace Matrix
26+
27+
variable {π•œ m n : Type*} {A : Matrix n n π•œ} [RCLike π•œ]
28+
29+
/-- The diagonal elements of a complex Hermitian matrix are real. -/
30+
lemma IsHermitian.coe_re_apply_self (h : A.IsHermitian) (i : n) : (re (A i i) : π•œ) = A i i := by
31+
rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]
32+
33+
/-- The diagonal elements of a complex Hermitian matrix are real. -/
34+
lemma IsHermitian.coe_re_diag (h : A.IsHermitian) : (fun i => (re (A.diag i) : π•œ)) = A.diag :=
35+
funext h.coe_re_apply_self
36+
37+
/-- A matrix is Hermitian iff the corresponding linear map is self adjoint. -/
38+
lemma isHermitian_iff_isSymmetric [Fintype n] [DecidableEq n] :
39+
IsHermitian A ↔ A.toEuclideanLin.IsSymmetric := by
40+
rw [LinearMap.IsSymmetric, (WithLp.toLp_surjective _).forallβ‚‚]
41+
simp only [toEuclideanLin_toLp, Matrix.toLin'_apply, EuclideanSpace.inner_eq_star_dotProduct,
42+
star_mulVec]
43+
constructor
44+
Β· rintro (h : Aα΄΄ = A) x y
45+
rw [dotProduct_comm, ← dotProduct_mulVec, h, dotProduct_comm]
46+
Β· intro h
47+
ext i j
48+
simpa [(Pi.single_star i 1).symm] using h (Pi.single i 1) (Pi.single j 1)
49+
50+
lemma IsHermitian.im_star_dotProduct_mulVec_self [Fintype n] (hA : A.IsHermitian) (x : n β†’ π•œ) :
51+
RCLike.im (star x ⬝α΅₯ A *α΅₯ x) = 0 := by
52+
classical
53+
simpa [dotProduct_comm] using (isHermitian_iff_isSymmetric.mp hA).im_inner_self_apply _
54+
55+
end Matrix

β€ŽMathlib/LinearAlgebra/Matrix/LDL.leanβ€Ž renamed to β€ŽMathlib/Analysis/Matrix/LDL.leanβ€Ž

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Alexander Bentkamp
55
-/
66
import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
7-
import Mathlib.LinearAlgebra.Matrix.PosDef
7+
import Mathlib.Analysis.Matrix.PosDef
88

99
/-! # LDL decomposition
1010

β€ŽMathlib/Analysis/Matrix/PosDef.leanβ€Ž

Lines changed: 47 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -7,22 +7,28 @@ import Mathlib.Analysis.Matrix.Spectrum
77
import Mathlib.LinearAlgebra.Matrix.PosDef
88

99
/-!
10-
# Spectrum of positive definite matrices
10+
# Spectrum of positive (semi)definite matrices
1111
1212
This file proves that eigenvalues of positive (semi)definite matrices are (nonnegative) positive.
13+
14+
## Main definitions
15+
16+
* `InnerProductSpace.ofMatrix`: the inner product on `n β†’ π•œ` induced by a positive definite
17+
matrix `A`, and is given by `βŸͺx, y⟫ = xα΄΄My`.
18+
1319
-/
1420

1521
open WithLp Matrix Unitary
1622
open scoped ComplexOrder
1723

1824
namespace Matrix
19-
variable {m n π•œ : Type*} [Fintype m] [Fintype n] [RCLike π•œ]
25+
variable {m n π•œ : Type*} [Fintype m] [Fintype n] [RCLike π•œ] {A : Matrix n n π•œ}
2026

2127
/-! ### Positive semidefinite matrices -/
2228

2329
/-- A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative. -/
24-
lemma IsHermitian.posSemidef_iff_eigenvalues_nonneg [DecidableEq n] {A : Matrix n n π•œ}
25-
(hA : IsHermitian A) : PosSemidef A ↔ 0 ≀ hA.eigenvalues := by
30+
lemma IsHermitian.posSemidef_iff_eigenvalues_nonneg [DecidableEq n] (hA : IsHermitian A) :
31+
PosSemidef A ↔ 0 ≀ hA.eigenvalues := by
2632
conv_lhs => rw [hA.spectral_theorem]
2733
simp [isUnit_coe.posSemidef_star_right_conjugate_iff, posSemidef_diagonal_iff, Pi.le_def]
2834

@@ -32,17 +38,17 @@ lemma IsHermitian.posSemidef_iff_eigenvalues_nonneg [DecidableEq n] {A : Matrix
3238
namespace PosSemidef
3339

3440
/-- The eigenvalues of a positive semi-definite matrix are non-negative -/
35-
lemma eigenvalues_nonneg [DecidableEq n] {A : Matrix n n π•œ}
36-
(hA : Matrix.PosSemidef A) (i : n) : 0 ≀ hA.1.eigenvalues i :=
41+
lemma eigenvalues_nonneg [DecidableEq n] (hA : A.PosSemidef) (i : n) : 0 ≀ hA.1.eigenvalues i :=
3742
hA.isHermitian.posSemidef_iff_eigenvalues_nonneg.mp hA _
3843

39-
lemma det_nonneg [DecidableEq n] {M : Matrix n n π•œ} (hM : M.PosSemidef) :
40-
0 ≀ M.det := by
41-
rw [hM.isHermitian.det_eq_prod_eigenvalues]
42-
exact Finset.prod_nonneg fun i _ ↦ by simpa using hM.eigenvalues_nonneg i
44+
lemma re_dotProduct_nonneg (hA : A.PosSemidef) (x : n β†’ π•œ) : 0 ≀ RCLike.re (star x ⬝α΅₯ (A *α΅₯ x)) :=
45+
RCLike.nonneg_iff.mp (hA.2 _) |>.1
46+
47+
lemma det_nonneg [DecidableEq n] (hA : A.PosSemidef) : 0 ≀ A.det := by
48+
rw [hA.isHermitian.det_eq_prod_eigenvalues]
49+
exact Finset.prod_nonneg fun i _ ↦ by simpa using hA.eigenvalues_nonneg i
4350

44-
lemma trace_eq_zero_iff {A : Matrix n n π•œ} (hA : A.PosSemidef) :
45-
A.trace = 0 ↔ A = 0 := by
51+
lemma trace_eq_zero_iff (hA : A.PosSemidef) : A.trace = 0 ↔ A = 0 := by
4652
classical
4753
conv_lhs => rw [hA.1.spectral_theorem, conjStarAlgAut_apply, trace_mul_cycle, coe_star_mul_self,
4854
one_mul, trace_diagonal, Finset.sum_eq_zero_iff_of_nonneg (by simp [hA.eigenvalues_nonneg])]
@@ -61,23 +67,45 @@ lemma eigenvalues_self_mul_conjTranspose_nonneg (A : Matrix m n π•œ) [Decidable
6167
/-! ### Positive definite matrices -/
6268

6369
/-- A Hermitian matrix is positive-definite if and only if its eigenvalues are positive. -/
64-
lemma IsHermitian.posDef_iff_eigenvalues_pos [DecidableEq n] {A : Matrix n n π•œ}
65-
(hA : A.IsHermitian) : A.PosDef ↔ βˆ€ i, 0 < hA.eigenvalues i := by
70+
lemma IsHermitian.posDef_iff_eigenvalues_pos [DecidableEq n] (hA : A.IsHermitian) :
71+
A.PosDef ↔ βˆ€ i, 0 < hA.eigenvalues i := by
6672
conv_lhs => rw [hA.spectral_theorem]
6773
simp [isUnit_coe.posDef_star_right_conjugate_iff]
6874

6975
namespace PosDef
7076

77+
lemma re_dotProduct_pos (hA : A.PosDef) {x : n β†’ π•œ} (hx : x β‰  0) :
78+
0 < RCLike.re (star x ⬝α΅₯ (A *α΅₯ x)) := RCLike.pos_iff.mp (hA.2 _ hx) |>.1
79+
7180
/-- The eigenvalues of a positive definite matrix are positive. -/
72-
lemma eigenvalues_pos [DecidableEq n] {A : Matrix n n π•œ}
73-
(hA : Matrix.PosDef A) (i : n) : 0 < hA.1.eigenvalues i :=
81+
lemma eigenvalues_pos [DecidableEq n] (hA : A.PosDef) (i : n) : 0 < hA.1.eigenvalues i :=
7482
hA.isHermitian.posDef_iff_eigenvalues_pos.mp hA i
7583

76-
lemma det_pos [DecidableEq n] {M : Matrix n n π•œ} (hM : M.PosDef) : 0 < det M := by
77-
rw [hM.isHermitian.det_eq_prod_eigenvalues]
84+
lemma det_pos [DecidableEq n] (hA : A.PosDef) : 0 < det A := by
85+
rw [hA.isHermitian.det_eq_prod_eigenvalues]
7886
apply Finset.prod_pos
7987
intro i _
80-
simpa using hM.eigenvalues_pos i
88+
simpa using hA.eigenvalues_pos i
8189

8290
end PosDef
91+
92+
/-- A positive definite matrix `A` induces a norm `β€–xβ€– = sqrt (re xα΄΄Mx)`. -/
93+
noncomputable abbrev NormedAddCommGroup.ofMatrix (hA : A.PosDef) : NormedAddCommGroup (n β†’ π•œ) :=
94+
@InnerProductSpace.Core.toNormedAddCommGroup _ _ _ _ _
95+
{ inner x y := (A *α΅₯ y) ⬝α΅₯ star x
96+
conj_inner_symm x y := by
97+
rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
98+
star_mulVec, dotProduct_comm (A *α΅₯ y), dotProduct_mulVec, hA.isHermitian.eq]
99+
re_inner_nonneg x := dotProduct_comm _ (star x) β–Έ hA.posSemidef.re_dotProduct_nonneg x
100+
definite x (hx : _ ⬝α΅₯ _ = 0) := by
101+
by_contra! h
102+
simpa [hx, lt_irrefl, dotProduct_comm] using hA.re_dotProduct_pos h
103+
add_left := by simp only [star_add, dotProduct_add, forall_const]
104+
smul_left _ _ _ := by rw [← smul_eq_mul, ← dotProduct_smul, starRingEnd_apply, ← star_smul] }
105+
106+
/-- A positive definite matrix `A` induces an inner product `βŸͺx, y⟫ = xα΄΄My`. -/
107+
def InnerProductSpace.ofMatrix (hA : A.PosDef) :
108+
@InnerProductSpace π•œ (n β†’ π•œ) _ (NormedAddCommGroup.ofMatrix hA).toSeminormedAddCommGroup :=
109+
InnerProductSpace.ofCore _
110+
83111
end Matrix

β€ŽMathlib/Analysis/Matrix/Spectrum.leanβ€Ž

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,12 +5,10 @@ Authors: Alexander Bentkamp
55
-/
66
import Mathlib.Algebra.Star.UnitaryStarAlgAut
77
import Mathlib.Analysis.InnerProductSpace.Spectrum
8+
import Mathlib.Analysis.Matrix.Hermitian
89
import Mathlib.LinearAlgebra.Eigenspace.Matrix
910
import Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
10-
import Mathlib.LinearAlgebra.Matrix.Diagonal
11-
import Mathlib.LinearAlgebra.Matrix.Hermitian
1211
import Mathlib.LinearAlgebra.Matrix.Rank
13-
import Mathlib.Topology.Algebra.Module.FiniteDimension
1412

1513
/-! # Spectral theory of Hermitian matrices
1614

β€ŽMathlib/LinearAlgebra/Matrix/Hermitian.leanβ€Ž

Lines changed: 5 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,7 @@ Copyright (c) 2022 Alexander Bentkamp. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Alexander Bentkamp
55
-/
6-
import Mathlib.Analysis.InnerProductSpace.PiL2
7-
import Mathlib.LinearAlgebra.Matrix.ConjTranspose
6+
import Mathlib.Algebra.Star.Pi
87
import Mathlib.LinearAlgebra.Matrix.ZPow
98

109
/-! # Hermitian matrices
@@ -23,14 +22,13 @@ self-adjoint matrix, hermitian matrix
2322
2423
-/
2524

25+
-- TODO:
26+
-- assert_not_exists MonoidAlgebra
27+
assert_not_exists NormedGroup
2628

2729
namespace Matrix
2830

29-
variable {Ξ± Ξ² : Type*} {m n : Type*} {A : Matrix n n Ξ±}
30-
31-
open scoped Matrix
32-
33-
local notation "βŸͺ" x ", " y "⟫" => inner Ξ± x y
31+
variable {Ξ± Ξ² m n : Type*} {A : Matrix n n Ξ±}
3432

3533
section Star
3634

@@ -307,40 +305,4 @@ end IsHermitian
307305
end SchurComplement
308306

309307
end CommRing
310-
311-
section RCLike
312-
313-
open RCLike
314-
315-
variable [RCLike Ξ±]
316-
317-
/-- The diagonal elements of a complex Hermitian matrix are real. -/
318-
theorem IsHermitian.coe_re_apply_self {A : Matrix n n Ξ±} (h : A.IsHermitian) (i : n) :
319-
(re (A i i) : Ξ±) = A i i := by rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]
320-
321-
/-- The diagonal elements of a complex Hermitian matrix are real. -/
322-
theorem IsHermitian.coe_re_diag {A : Matrix n n Ξ±} (h : A.IsHermitian) :
323-
(fun i => (re (A.diag i) : Ξ±)) = A.diag :=
324-
funext h.coe_re_apply_self
325-
326-
/-- A matrix is Hermitian iff the corresponding linear map is self adjoint. -/
327-
theorem isHermitian_iff_isSymmetric [Fintype n] [DecidableEq n] {A : Matrix n n Ξ±} :
328-
IsHermitian A ↔ A.toEuclideanLin.IsSymmetric := by
329-
rw [LinearMap.IsSymmetric, (WithLp.toLp_surjective _).forallβ‚‚]
330-
simp only [toEuclideanLin_toLp, Matrix.toLin'_apply, EuclideanSpace.inner_eq_star_dotProduct,
331-
star_mulVec]
332-
constructor
333-
Β· rintro (h : Aα΄΄ = A) x y
334-
rw [dotProduct_comm, ← dotProduct_mulVec, h, dotProduct_comm]
335-
Β· intro h
336-
ext i j
337-
simpa [(Pi.single_star i 1).symm] using h (Pi.single i 1) (Pi.single j 1)
338-
339-
theorem IsHermitian.im_star_dotProduct_mulVec_self [Fintype n] {A : Matrix n n Ξ±}
340-
(hA : A.IsHermitian) (x : n β†’ Ξ±) : RCLike.im (star x ⬝α΅₯ A *α΅₯ x) = 0 := by
341-
classical
342-
exact dotProduct_comm _ (star x) β–Έ (isHermitian_iff_isSymmetric.mp hA).im_inner_self_apply _
343-
344-
end RCLike
345-
346308
end Matrix

β€ŽMathlib/LinearAlgebra/Matrix/PosDef.leanβ€Ž

Lines changed: 5 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,9 @@ Copyright (c) 2022 Alexander Bentkamp. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Alexander Bentkamp, Mohanad Ahmed
55
-/
6+
import Mathlib.Algebra.CharP.Invertible
67
import Mathlib.Algebra.Order.Ring.Star
8+
import Mathlib.Data.Real.Star
79
import Mathlib.LinearAlgebra.Matrix.DotProduct
810
import Mathlib.LinearAlgebra.Matrix.Hermitian
911
import Mathlib.LinearAlgebra.Matrix.Vec
@@ -35,20 +37,16 @@ order on matrices on `ℝ` or `β„‚`.
3537

3638
-- TODO:
3739
-- assert_not_exists MonoidAlgebra
38-
assert_not_exists Matrix.IsHermitian.eigenvalues
40+
assert_not_exists NormedGroup
3941

40-
open WithLp
41-
42-
open scoped ComplexOrder
42+
open Matrix
4343

4444
namespace Matrix
4545

46-
variable {m n R R' π•œ : Type*}
46+
variable {m n R R' : Type*}
4747
variable [Fintype m] [Fintype n]
4848
variable [Ring R] [PartialOrder R] [StarRing R]
4949
variable [CommRing R'] [PartialOrder R'] [StarRing R']
50-
variable [RCLike π•œ]
51-
open Matrix
5250

5351
/-!
5452
## Positive semidefinite matrices
@@ -76,10 +74,6 @@ namespace PosSemidef
7674
theorem isHermitian {M : Matrix n n R} (hM : M.PosSemidef) : M.IsHermitian :=
7775
hM.1
7876

79-
theorem re_dotProduct_nonneg {M : Matrix n n π•œ} (hM : M.PosSemidef) (x : n β†’ π•œ) :
80-
0 ≀ RCLike.re (star x ⬝α΅₯ (M *α΅₯ x)) :=
81-
RCLike.nonneg_iff.mp (hM.2 _) |>.1
82-
8377
lemma conjTranspose_mul_mul_same {A : Matrix n n R} (hA : PosSemidef A)
8478
{m : Type*} [Fintype m] (B : Matrix n m R) :
8579
PosSemidef (Bα΄΄ * A * B) := by
@@ -279,10 +273,6 @@ namespace PosDef
279273
theorem isHermitian {M : Matrix n n R} (hM : M.PosDef) : M.IsHermitian :=
280274
hM.1
281275

282-
theorem re_dotProduct_pos {M : Matrix n n π•œ} (hM : M.PosDef) {x : n β†’ π•œ} (hx : x β‰  0) :
283-
0 < RCLike.re (star x ⬝α΅₯ (M *α΅₯ x)) :=
284-
RCLike.pos_iff.mp (hM.2 _ hx) |>.1
285-
286276
theorem posSemidef {M : Matrix n n R} (hM : M.PosDef) : M.PosSemidef := by
287277
refine ⟨hM.1, ?_⟩
288278
intro x
@@ -551,28 +541,3 @@ theorem posDef_toMatrix' [DecidableEq n] {Q : QuadraticForm ℝ (n β†’ ℝ)} (hQ
551541
exact .of_toQuadraticForm' (isSymm_toMatrix' Q) hQ
552542

553543
end QuadraticForm
554-
555-
namespace Matrix
556-
variable {π•œ : Type*} [RCLike π•œ] {n : Type*} [Fintype n]
557-
558-
/-- A positive definite matrix `M` induces a norm `β€–xβ€– = sqrt (re xα΄΄Mx)`. -/
559-
noncomputable abbrev NormedAddCommGroup.ofMatrix {M : Matrix n n π•œ} (hM : M.PosDef) :
560-
NormedAddCommGroup (n β†’ π•œ) :=
561-
@InnerProductSpace.Core.toNormedAddCommGroup _ _ _ _ _
562-
{ inner x y := (M *α΅₯ y) ⬝α΅₯ star x
563-
conj_inner_symm x y := by
564-
rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
565-
star_mulVec, dotProduct_comm (M *α΅₯ y), dotProduct_mulVec, hM.isHermitian.eq]
566-
re_inner_nonneg x := dotProduct_comm _ (star x) β–Έ hM.posSemidef.re_dotProduct_nonneg x
567-
definite x (hx : _ ⬝α΅₯ _ = 0) := by
568-
by_contra! h
569-
simpa [hx, lt_irrefl, dotProduct_comm] using hM.re_dotProduct_pos h
570-
add_left := by simp only [star_add, dotProduct_add, forall_const]
571-
smul_left _ _ _ := by rw [← smul_eq_mul, ← dotProduct_smul, starRingEnd_apply, ← star_smul] }
572-
573-
/-- A positive definite matrix `M` induces an inner product `βŸͺx, y⟫ = xα΄΄My`. -/
574-
def InnerProductSpace.ofMatrix {M : Matrix n n π•œ} (hM : M.PosDef) :
575-
@InnerProductSpace π•œ (n β†’ π•œ) _ (NormedAddCommGroup.ofMatrix hM).toSeminormedAddCommGroup :=
576-
InnerProductSpace.ofCore _
577-
578-
end Matrix

0 commit comments

Comments
Β (0)