Theorem Matrix.posSemidef_self_mul_conjTranspose

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_self_mul_conjTransposeView on Github →
2024-05-31 00:19
Mathlib/LinearAlgebra/Matrix/PosDef.lean
chore: fix formatting of many misplaced "by"s (#13204)
Modified Matrix.posSemidef_self_mul_conjTransposeView 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_self_mul_conjTransposeView on Github →
2023-08-16 16:11
Mathlib/LinearAlgebra/Matrix/PosDef.lean
refactor(LinearAlgebra/Matrix/PosDef): Generalize to StarOrderedRing (#6489) …
Modified Matrix.posSemidef_self_mul_conjTransposeView 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_self_mul_conjTransposeView 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_self_mul_conjTransposeView on Github →