Theorem Matrix.posSemidef_conjTranspose_mul_self

Modification history

2024-08-12 18:29
Mathlib/LinearAlgebra/Matrix/PosDef.lean
chore: move to v4.11.0-rc2 (new `variable` command) (#15726)
Modified Matrix.posSemidef_conjTranspose_mul_selfView on Github →
2023-12-18 20:33
Mathlib/LinearAlgebra/Matrix/PosDef.lean
feat(LinearAlgebra/Matrix/PosDef): unique positive semidef square root (#8809) …
Modified Matrix.posSemidef_conjTranspose_mul_selfView on Github →
2023-08-16 16:11
Mathlib/LinearAlgebra/Matrix/PosDef.lean
refactor(LinearAlgebra/Matrix/PosDef): Generalize to StarOrderedRing (#6489) …
Modified Matrix.posSemidef_conjTranspose_mul_selfView on Github →
2023-08-16 09:33
Mathlib/LinearAlgebra/Matrix/PosDef.lean
refactor(Data/Matrix): Eliminate `⬝` notation in favor of `HMul` (#6487) …
Modified Matrix.posSemidef_conjTranspose_mul_selfView on Github →
2023-08-04 16:36
Mathlib/LinearAlgebra/Matrix/PosDef.lean
ConjTranspose multiplication of a matrix by itself is Positive Semidefinite (#6359) …
Added Matrix.posSemidef_conjTranspose_mul_selfView on Github →