Skip to content

Commit 430b300

Browse files
committed
remove docstring
1 parent b4ac9e3 commit 430b300

1 file changed

Lines changed: 0 additions & 2 deletions

File tree

Mathlib/LinearAlgebra/Matrix/PosDef.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,6 @@ of quadratic forms. Most results require `𝕜 = ℝ` or `ℂ`.
2222
2323
## Main results
2424
25-
* `Matrix.instPartialOrder`: the partial order on matrices
26-
* `Matrix.instStarOrderedRing`: the star ordered ring instance on matrices
2725
* `Matrix.posDef_iff_eq_conjTranspose_mul_self`: a matrix `M : Matrix n n 𝕜` is positive
2826
definite iff it has the form `Bᴴ * B` for some _invertible_ `B`.
2927
-/

0 commit comments

Comments
 (0)