PosDef

📁 Source: Mathlib/LinearAlgebra/Matrix/PosDef.lean

Statistics

Metric	Count
Definitions `PosDef`, `PosSemidef`, `PosDef`	3
Theorems `posDef_star_left_conjugate_iff`, `posDef_star_right_conjugate_iff`, `posSemidef_star_left_conjugate_iff`, `posSemidef_star_right_conjugate_iff`, `add`, `add_posSemidef`, `conjTranspose`, `conjTranspose_mul_mul_same`, `conjTranspose_mul_self`, `diag_pos`, `diagonal`, `dotProduct_mulVec_pos`, `fromBlocks₁₁`, `fromBlocks₂₂`, `intCast`, `inv`, `isHermitian`, `isUnit`, `mul_conjTranspose_self`, `mul_mul_conjTranspose_same`, `natCast`, `ofNat`, `of_dotProduct_mulVec_pos`, `of_subsingleton`, `of_toQuadraticForm'`, `one`, `posSemidef`, `posSemidef_add`, `smul`, `submatrix`, `toQuadraticForm'`, `trace_pos`, `transpose`, `transpose_iff`, `add`, `conjTranspose`, `conjTranspose_mul_mul_same`, `diag_nonneg`, `diagonal`, `dotProduct_mulVec_nonneg`, `intCast`, `inv`, `isHermitian`, `mul_mul_conjTranspose_same`, `natCast`, `ofNat`, `of_dotProduct_mulVec_nonneg`, `one`, `pow`, `smul`, `submatrix`, `trace_nonneg`, `transpose`, `zero`, `zpow`, `posDef_conjTranspose_iff`, `posDef_diagonal_iff`, `posDef_iff_dotProduct_mulVec`, `posDef_intCast_iff`, `posDef_inv_iff`, `posDef_natCast_iff`, `posDef_sum`, `posSemidef_conjTranspose_iff`, `posSemidef_conjTranspose_mul_self`, `posSemidef_diagonal_iff`, `posSemidef_iff_dotProduct_mulVec`, `posSemidef_intCast_iff`, `posSemidef_self_mul_conjTranspose`, `posSemidef_submatrix_equiv`, `posSemidef_sum`, `posSemidef_transpose_iff`, `posSemidef_vecMulVec_self_star`, `posSemidef_vecMulVec_star_self`, `trace_conjTranspose_mul_self_eq_zero_iff`, `trace_mul_conjTranspose_self_eq_zero_iff`, `posDef_of_toMatrix'`, `posDef_toMatrix'`	77
Total	80

Matrix

Definitions

Name	Category	Theorems
`PosDef` 📖	MathDef	41 math math: `QuadraticForm.posDef_toMatrix'`, `posDef_iff_dotProduct_mulVec`, `PosDef.ofNat`, `PosDef.posSemidef_add`, `PosDef.add`, `PosSemidef.posDef_iff_isUnit`, `PosDef.conjTranspose_mul_mul_same`, `PosDef.natCast`, `PosDef.of_subsingleton`, `posDef_gram_of_linearIndependent`, `PosDef.one`, `posDef_conjTranspose_iff`, `posDef_gram_iff_linearIndependent`, `PosDef.submatrix`, `PosDef.conjTranspose_mul_self`, `isStrictlyPositive_iff_posDef`, `PosDef.commute_iff`, `PosDef.transpose_iff`, `posDef_iff_eq_conjTranspose_mul_self`, `posDef_sum`, `PosDef.of_toQuadraticForm'`, `PosDef.add_posSemidef`, `PosDef.kronecker`, `posDef_natCast_iff`, `PosDef.transpose`, `posDef_inv_iff`, `posDef_intCast_iff`, `PosDef.mul_mul_conjTranspose_same`, `PosDef.diagonal`, `IsHermitian.posDef_iff_eigenvalues_pos`, `PosDef.intCast`, `IsStrictlyPositive.posDef`, `PosDef.smul`, `IsUnit.posDef_star_left_conjugate_iff`, `PosDef.posDef_sqrt`, `PosDef.of_dotProduct_mulVec_pos`, `PosDef.mul_conjTranspose_self`, `posDef_diagonal_iff`, `PosDef.conjTranspose`, `PosDef.inv`, `IsUnit.posDef_star_right_conjugate_iff`
`PosSemidef` 📖	MathDef	47 math math: `posSemidef_conjTranspose_mul_self`, `le_iff`, `posSemidef_self_mul_conjTranspose`, `PosSemidef.transpose`, `PosSemidef.intCast`, `PosSemidef.natCast`, `IsUnit.posSemidef_star_right_conjugate_iff`, `PosDef.fromBlocks₁₁`, `PosSemidef.conjTranspose_mul_mul_same`, `SimpleGraph.posSemidef_lapMatrix`, `posSemidef_vecMulVec_self_star`, `PosSemidef.one`, `RKHS.posSemidef_tfae`, `LE.le.posSemidef`, `PosSemidef.diagonal`, `LinearMap.isPosSemidef_iff_posSemidef_toMatrix`, `PosSemidef.mul_mul_conjTranspose_same`, `IsHermitian.posSemidef_iff_eigenvalues_nonneg`, `nonneg_iff_posSemidef`, `PosSemidef.add`, `isPositive_toEuclideanLin_iff`, `posSemidef_vecMulVec_star_self`, `PosSemidef.zero`, `PosSemidef.kronecker`, `PosSemidef.conjTranspose`, `posSemidef_gram`, `PosDef.fromBlocks₂₂`, `PosSemidef.zpow`, `posSemidef_transpose_iff`, `PosSemidef.pow`, `posSemidef_sum`, `posSemidef_intCast_iff`, `posSemidef_iff_eq_sum_vecMulVec`, `PosDef.posSemidef`, `posSemidef_iff_dotProduct_mulVec`, `PosSemidef.submatrix`, `posSemidef_diagonal_iff`, `PosSemidef.ofNat`, `IsUnit.posSemidef_star_left_conjugate_iff`, `PosSemidef.of_dotProduct_mulVec_nonneg`, `PosSemidef.smul`, `PosSemidef.inv`, `LinearMap.posSemidef_toMatrix_iff`, `posSemidef_submatrix_equiv`, `RKHS.posSemidef_kernel`, `posSemidef_conjTranspose_iff`, `posSemidef_iff_isHermitian_and_spectrum_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`posDef_conjTranspose_iff` 📖	mathematical	—	`PosDef` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid`	—	`conjTranspose_conjTranspose` `PosDef.conjTranspose`
`posDef_diagonal_iff` 📖	mathematical	—	`PosDef` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Preorder.toLT` `PartialOrder.toPreorder`	—	`NeZero.one` `Finsupp.sum_single_index` `MulZeroClass.mul_zero` `mul_one` `star_zero` `diagonal_apply_eq` `MulZeroClass.zero_mul` `star_one` `one_mul` `PosDef.diagonal`
`posDef_iff_dotProduct_mulVec` 📖	mathematical	—	`PosDef` `IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `Pi.instStarForall` `mulVec`	—	`Finite.of_fintype` `Finsupp.coe_eq_zero` `mul_assoc` `Finsupp.sum_fintype` `MulZeroClass.mul_zero` `Finset.sum_congr` `star_zero` `MulZeroClass.zero_mul` `Finset.sum_const_zero` `Finset.mul_sum` `Equiv.forall_congr_right`
`posDef_intCast_iff` 📖	mathematical	—	`PosDef` `Matrix` `instIntCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`posDef_diagonal_iff` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `instZeroLEOneClass` `NeZero.one`
`posDef_inv_iff` 📖	mathematical	—	`PosDef` `DivisionRing.toRing` `Field.toDivisionRing` `Matrix` `inv` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`PosDef.inv` `inv_inv_of_invertible` `isUnit_nonsing_inv_iff` `PosDef.isUnit`
`posDef_natCast_iff` 📖	mathematical	—	`PosDef` `Matrix` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`posDef_diagonal_iff` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `instZeroLEOneClass` `NeZero.one`
`posDef_sum` 📖	mathematical	`Finset.Nonempty` `PosDef`	`PosDef` `Finset.sum` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Finset.induction_on` `Finset.sum_insert` `Finset.sum_congr` `add_zero` `PosDef.add` `Finset.mem_insert_self` `Finset.mem_insert_of_mem`
`posSemidef_conjTranspose_iff` 📖	mathematical	—	`PosSemidef` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid`	—	`conjTranspose_conjTranspose` `PosSemidef.conjTranspose`
`posSemidef_conjTranspose_mul_self` 📖	mathematical	—	`PosSemidef` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`PosSemidef.of_dotProduct_mulVec_nonneg` `isHermitian_conjTranspose_mul_self` `mulVec_mulVec` `dotProduct_mulVec` `vecMul_conjTranspose` `star_star` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `star_mul_self_nonneg`
`posSemidef_diagonal_iff` 📖	mathematical	—	`PosSemidef` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Preorder.toLE` `PartialOrder.toPreorder`	—	`Finsupp.sum_single_index` `MulZeroClass.mul_zero` `mul_one` `star_zero` `diagonal_apply_eq` `MulZeroClass.zero_mul` `star_one` `one_mul` `PosSemidef.diagonal`
`posSemidef_iff_dotProduct_mulVec` 📖	mathematical	—	`PosSemidef` `IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `Pi.instStarForall` `mulVec`	—	`mul_assoc` `Finsupp.sum_fintype` `MulZeroClass.mul_zero` `Finset.sum_congr` `star_zero` `MulZeroClass.zero_mul` `Finset.sum_const_zero` `Finite.of_fintype` `Finset.mul_sum` `Equiv.forall_congr_right`
`posSemidef_intCast_iff` 📖	mathematical	—	`PosSemidef` `Matrix` `instIntCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `instZeroLEOneClass` `NeZero.one`
`posSemidef_self_mul_conjTranspose` 📖	mathematical	—	`PosSemidef` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`conjTranspose_conjTranspose` `posSemidef_conjTranspose_mul_self`
`posSemidef_submatrix_equiv` 📖	mathematical	—	`PosSemidef` `submatrix` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`submatrix_submatrix` `Equiv.self_comp_symm` `submatrix_id_id` `PosSemidef.submatrix`
`posSemidef_sum` 📖	mathematical	`PosSemidef`	`PosSemidef` `Finset.sum` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`isSelfAdjoint_sum` `sum_apply` `Finset.mul_sum` `Finset.sum_mul` `Finsupp.sum_finsetSum_comm` `Finset.sum_nonneg`
`posSemidef_transpose_iff` 📖	mathematical	—	`PosSemidef` `CommRing.toRing` `transpose`	—	`PosSemidef.transpose`
`posSemidef_vecMulVec_self_star` 📖	mathematical	—	`PosSemidef` `vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`vecMulVec_eq`
`posSemidef_vecMulVec_star_self` 📖	mathematical	—	`PosSemidef` `vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`vecMulVec_eq`
`trace_conjTranspose_mul_self_eq_zero_iff` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `zero`	—	`star_vec_dotProduct_vec` `dotProduct_star_self_eq_zero` `vec_eq_zero_iff`
`trace_mul_conjTranspose_self_eq_zero_iff` 📖	mathematical	—	`trace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `zero`	—	`conjTranspose_conjTranspose` `trace_conjTranspose_mul_self_eq_zero_iff`

Matrix.IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`posDef_star_left_conjugate_iff` 📖	mathematical	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring`	`Matrix.PosDef` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`CanLift.prf` `instCanLiftUnitsValIsUnit` `Matrix.PosDef.conjTranspose_mul_mul_same` `Matrix.mulVec_injective_of_isUnit` `Units.isUnit` `one_mul` `star_one` `mul_one` `Units.mul_inv` `mul_assoc` `Matrix.star_mul` `Matrix.star_eq_conjTranspose`
`posDef_star_right_conjugate_iff` 📖	mathematical	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring`	`Matrix.PosDef` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`star_star` `posDef_star_left_conjugate_iff` `IsUnit.star`
`posSemidef_star_left_conjugate_iff` 📖	mathematical	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring`	`Matrix.PosSemidef` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`CanLift.prf` `instCanLiftUnitsValIsUnit` `Matrix.PosSemidef.conjTranspose_mul_mul_same` `Finite.of_fintype` `one_mul` `star_one` `mul_one` `Units.mul_inv` `mul_assoc` `Matrix.star_mul` `Matrix.star_eq_conjTranspose`
`posSemidef_star_right_conjugate_iff` 📖	mathematical	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring`	`Matrix.PosSemidef` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `Matrix.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`star_star` `posSemidef_star_left_conjugate_iff` `IsUnit.star`

Matrix.PosDef

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Matrix.PosDef`	`Matrix.PosDef` `Matrix` `Matrix.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`add_posSemidef` `posSemidef`
`add_posSemidef` 📖	mathematical	`Matrix.PosDef` `Matrix.PosSemidef`	`Matrix.PosDef` `Matrix` `Matrix.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Matrix.IsHermitian.add` `isHermitian` `Matrix.PosSemidef.isHermitian` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `Finsupp.sum_add` `add_pos_of_pos_of_nonneg`
`conjTranspose` 📖	mathematical	`Matrix.PosDef`	`Matrix.PosDef` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid`	—	—
`conjTranspose_mul_mul_same` 📖	mathematical	`Matrix.PosDef` `Matrix.mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Matrix.PosDef` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`of_dotProduct_mulVec_pos` `Matrix.isHermitian_conjTranspose_mul_mul` `Matrix.mulVec_zero` `Matrix.dotProduct_mulVec` `Matrix.star_mulVec` `Matrix.vecMul_vecMul` `dotProduct_mulVec_pos`
`conjTranspose_mul_self` 📖	mathematical	`Matrix.mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Matrix.PosDef` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`Matrix.mul_one` `conjTranspose_mul_mul_same` `one`
`diag_pos` 📖	mathematical	`Matrix.PosDef`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`NeZero.one` `Finsupp.sum_single_index` `MulZeroClass.mul_zero` `mul_one` `star_zero` `MulZeroClass.zero_mul` `star_one` `one_mul`
`diagonal` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Matrix.PosDef` `Matrix.diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Matrix.isHermitian_diagonal_of_self_adjoint` `IsSelfAdjoint.of_nonneg` `LT.lt.le` `Finsupp.sum_pos'` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedAddMonoid.toAddLeftMono` `Finsupp.sum_nonneg` `MulZeroClass.mul_zero` `ite_mul` `MulZeroClass.zero_mul` `star_left_conjugate_nonneg` `instReflLe` `Finsupp.mem_support_iff` `star_left_conjugate_pos` `IsRegular.of_ne_zero` `NoZeroDivisors.to_isCancelMulZero`
`dotProduct_mulVec_pos` 📖	mathematical	`Matrix.PosDef`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `Matrix.mulVec`	—	`Matrix.posDef_iff_dotProduct_mulVec`
`fromBlocks₁₁` 📖	mathematical	`Matrix.PosDef` `CommRing.toRing`	`Matrix.PosSemidef` `CommRing.toRing` `Matrix.fromBlocks` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid` `Matrix` `Matrix.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Matrix.inv`	—	`Matrix.posSemidef_iff_dotProduct_mulVec` `Matrix.IsHermitian.fromBlocks₁₁` `Matrix.PosSemidef.of_dotProduct_mulVec_nonneg` `Matrix.dotProduct_mulVec` `zero_add` `dotProduct_zero` `neg_add_cancel` `Matrix.schur_complement_eq₁₁` `le_add_of_nonneg_of_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `StarOrderedRing.toIsOrderedRing` `posSemidef`
`fromBlocks₂₂` 📖	mathematical	`Matrix.PosDef` `CommRing.toRing`	`Matrix.PosSemidef` `CommRing.toRing` `Matrix.fromBlocks` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid` `Matrix` `Matrix.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Matrix.inv`	—	`Matrix.posSemidef_submatrix_equiv` `Equiv.sumComm_apply` `Matrix.fromBlocks_submatrix_sum_swap_sum_swap` `Matrix.conjTranspose_conjTranspose` `fromBlocks₁₁`
`intCast` 📖	mathematical	—	`Matrix.PosDef` `Matrix` `Matrix.instIntCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `diagonal` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `instZeroLEOneClass` `NeZero.one`
`inv` 📖	mathematical	`Matrix.PosDef` `DivisionRing.toRing` `Field.toDivisionRing`	`Matrix.PosDef` `DivisionRing.toRing` `Field.toDivisionRing` `Matrix` `Matrix.inv` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`mul_mul_conjTranspose_same` `isUnit` `Matrix.inv_mul_of_invertible` `one_mul` `Matrix.conjTranspose_conjTranspose` `conjTranspose`
`isHermitian` 📖	mathematical	`Matrix.PosDef`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid`	—	—
`isUnit` 📖	mathematical	`Matrix.PosDef` `DivisionRing.toRing` `Field.toDivisionRing`	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Function.not_injective_iff` `Iff.not` `Matrix.mulVec_injective_iff_isUnit` `Matrix.mulVec_sub` `sub_self` `dotProduct_zero` `dotProduct_mulVec_pos`
`mul_conjTranspose_self` 📖	mathematical	`Matrix.vecMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Matrix.PosDef` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`Matrix.mul_one` `mul_mul_conjTranspose_same` `one`
`mul_mul_conjTranspose_same` 📖	mathematical	`Matrix.PosDef` `Matrix.vecMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Matrix.PosDef` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`star_injective` `Matrix.conjTranspose_conjTranspose` `conjTranspose_mul_mul_same` `star_star` `Matrix.star_vecMul`
`natCast` 📖	mathematical	—	`Matrix.PosDef` `Matrix` `Matrix.instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `diagonal` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `instZeroLEOneClass` `NeZero.one` `Nat.instCanonicallyOrderedAdd`
`ofNat` 📖	mathematical	—	`Matrix.PosDef`	—	`natCast` `Nat.AtLeastTwo.toNeZero`
`of_dotProduct_mulVec_pos` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `Pi.instStarForall` `Matrix.mulVec`	`Matrix.PosDef`	—	`Matrix.posDef_iff_dotProduct_mulVec`
`of_subsingleton` 📖	mathematical	—	`Matrix.PosDef`	—	`Matrix.IsHermitian.of_subsingleton` `Finsupp.instSubsingleton'`
`of_toQuadraticForm'` 📖	mathematical	`Matrix.IsSymm` `Real` `QuadraticMap.PosDef` `CommRing.toCommSemiring` `Real.commRing` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `CommSemiring.toSemiring` `Semiring.toModule` `Real.partialOrder` `Matrix.toQuadraticMap'`	`Matrix.PosDef` `Real` `Real.instRing` `Real.partialOrder` `instStarRingReal`	—	`of_dotProduct_mulVec_pos` `Matrix.toLinearMap₂'_apply'`
`one` 📖	mathematical	—	`Matrix.PosDef` `Matrix` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `diagonal` `zero_lt_one'` `instZeroLEOneClass` `NeZero.one`
`posSemidef` 📖	mathematical	`Matrix.PosDef`	`Matrix.PosSemidef`	—	`eq_or_ne` `Finsupp.sum_fun_zero` `instReflLe`
`posSemidef_add` 📖	mathematical	`Matrix.PosSemidef` `Matrix.PosDef`	`Matrix.PosDef` `Matrix` `Matrix.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`add_posSemidef` `add_comm`
`smul` 📖	mathematical	`Matrix.PosDef` `Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`Matrix.PosDef` `Matrix` `Matrix.smul` `Algebra.toSMul` `Ring.toSemiring`	—	`IsSelfAdjoint.smul` `Matrix.instStarModule` `IsSelfAdjoint.of_nonneg` `LT.lt.le` `Algebra.mul_smul_comm` `Algebra.smul_mul_assoc` `smul_pos`
`submatrix` 📖	mathematical	`Matrix.PosDef`	`Matrix.PosDef` `Matrix.submatrix`	—	`Matrix.IsHermitian.submatrix` `Finsupp.sum_mapDomain_index` `MulZeroClass.mul_zero` `mul_add` `Distrib.leftDistribClass` `star_zero` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `StarAddMonoid.star_add` `add_mul` `Distrib.rightDistribClass` `Finsupp.sum_add` `Finsupp.mapDomain_injective` `Finsupp.mapDomain_zero`
`toQuadraticForm'` 📖	mathematical	`Matrix.PosDef` `Real` `Real.instRing` `Real.partialOrder` `instStarRingReal`	`QuadraticMap.PosDef` `Real` `CommRing.toCommSemiring` `Real.commRing` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `CommSemiring.toSemiring` `Semiring.toModule` `Real.partialOrder` `Matrix.toQuadraticMap'`	—	`Matrix.toLinearMap₂'_apply'` `dotProduct_mulVec_pos`
`trace_pos` 📖	mathematical	`Matrix.PosDef`	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Matrix.trace` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Finset.sum_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `diag_pos` `Finset.univ_nonempty`
`transpose` 📖	mathematical	`Matrix.PosDef` `CommRing.toRing`	`Matrix.PosDef` `CommRing.toRing` `Matrix.transpose`	—	`Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Matrix.IsHermitian.transpose` `Finsupp.sum_comm` `star_zero` `Finsupp.sum_mapRange_index` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `star_star`
`transpose_iff` 📖	mathematical	—	`Matrix.PosDef` `CommRing.toRing` `Matrix.transpose`	—	`Matrix.transpose_transpose` `transpose`

Matrix.PosSemidef

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Matrix.PosSemidef`	`Matrix.PosSemidef` `Matrix` `Matrix.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Matrix.IsHermitian.add` `isHermitian` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `Finsupp.sum_add` `add_nonneg`
`conjTranspose` 📖	mathematical	`Matrix.PosSemidef`	`Matrix.PosSemidef` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid`	—	—
`conjTranspose_mul_mul_same` 📖	mathematical	`Matrix.PosSemidef`	`Matrix.PosSemidef` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`of_dotProduct_mulVec_nonneg` `Matrix.isHermitian_conjTranspose_mul_mul` `Matrix.dotProduct_mulVec` `Matrix.star_mulVec` `Matrix.vecMul_vecMul` `dotProduct_mulVec_nonneg`
`diag_nonneg` 📖	mathematical	`Matrix.PosSemidef`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Finsupp.sum_single_index` `MulZeroClass.mul_zero` `mul_one` `star_zero` `MulZeroClass.zero_mul` `star_one` `one_mul`
`diagonal` 📖	mathematical	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Matrix.PosSemidef` `Matrix.diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Matrix.isHermitian_diagonal_of_self_adjoint` `IsSelfAdjoint.of_nonneg` `Finsupp.sum_nonneg` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `MulZeroClass.mul_zero` `ite_mul` `MulZeroClass.zero_mul` `star_left_conjugate_nonneg` `instReflLe`
`dotProduct_mulVec_nonneg` 📖	mathematical	`Matrix.PosSemidef`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `Matrix.mulVec`	—	`Matrix.posSemidef_iff_dotProduct_mulVec`
`intCast` 📖	mathematical	—	`Matrix.PosSemidef` `Matrix` `Matrix.instIntCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`Matrix.isHermitian_intCast` `Finsupp.sum_nonneg` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `eq_or_ne` `Matrix.diagonal_apply_eq` `IsOrderedAddMonoid.toAddLeftMono` `instZeroLEOneClass` `Matrix.diagonal_apply_ne` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `instReflLe`
`inv` 📖	mathematical	`Matrix.PosSemidef` `CommRing.toRing`	`Matrix.PosSemidef` `CommRing.toRing` `Matrix` `Matrix.inv`	—	`conjTranspose` `conjTranspose_mul_mul_same` `Finite.of_fintype` `Matrix.conjTranspose_conjTranspose` `Matrix.mul_nonsing_inv_cancel_right` `Matrix.nonsing_inv_apply_not_isUnit` `zero`
`isHermitian` 📖	mathematical	`Matrix.PosSemidef`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid`	—	—
`mul_mul_conjTranspose_same` 📖	mathematical	`Matrix.PosSemidef`	`Matrix.PosSemidef` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`Matrix.conjTranspose_conjTranspose` `conjTranspose_mul_mul_same`
`natCast` 📖	mathematical	—	`Matrix.PosSemidef` `Matrix` `Matrix.instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Matrix.isHermitian_natCast` `Finsupp.sum_nonneg` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `eq_or_ne` `Matrix.diagonal_apply_eq` `IsOrderedAddMonoid.toAddLeftMono` `instZeroLEOneClass` `Matrix.diagonal_apply_ne` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `instReflLe`
`ofNat` 📖	mathematical	—	`Matrix.PosSemidef`	—	`natCast`
`of_dotProduct_mulVec_nonneg` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `Pi.instStarForall` `Matrix.mulVec`	`Matrix.PosSemidef`	—	`Matrix.posSemidef_iff_dotProduct_mulVec`
`one` 📖	mathematical	—	`Matrix.PosSemidef` `Matrix` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Matrix.isHermitian_one` `Finsupp.sum_nonneg` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `eq_or_ne` `Matrix.one_apply_eq` `mul_one` `Matrix.one_apply_ne` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `instReflLe`
`pow` 📖	mathematical	`Matrix.PosSemidef`	`Matrix.PosSemidef` `Matrix` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Ring.toSemiring`	—	`one` `pow_one` `pow_succ` `pow_succ'` `Matrix.IsHermitian.eq` `isHermitian` `mul_mul_conjTranspose_same` `Finite.of_fintype`
`smul` 📖	mathematical	`Matrix.PosSemidef` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`Matrix.PosSemidef` `Matrix` `Matrix.smul` `Algebra.toSMul` `Ring.toSemiring`	—	`IsSelfAdjoint.smul` `Matrix.instStarModule` `IsSelfAdjoint.of_nonneg` `Algebra.mul_smul_comm` `Algebra.smul_mul_assoc` `smul_nonneg`
`submatrix` 📖	mathematical	`Matrix.PosSemidef`	`Matrix.PosSemidef` `Matrix.submatrix`	—	`Matrix.IsHermitian.submatrix` `Finsupp.sum_mapDomain_index` `MulZeroClass.mul_zero` `mul_add` `Distrib.leftDistribClass` `star_zero` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `StarAddMonoid.star_add` `add_mul` `Distrib.rightDistribClass` `Finsupp.sum_add`
`trace_nonneg` 📖	mathematical	`Matrix.PosSemidef`	`Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Matrix.trace` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Fintype.sum_nonneg` `diag_nonneg`
`transpose` 📖	mathematical	`Matrix.PosSemidef` `CommRing.toRing`	`Matrix.PosSemidef` `CommRing.toRing` `Matrix.transpose`	—	`Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Matrix.IsHermitian.transpose` `Finsupp.sum_comm` `star_zero` `Finsupp.sum_mapRange_index` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `star_star`
`zero` 📖	mathematical	—	`Matrix.PosSemidef` `Matrix` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Matrix.isHermitian_zero` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `Finsupp.sum_fun_zero` `instReflLe`
`zpow` 📖	mathematical	`Matrix.PosSemidef` `CommRing.toRing`	`Matrix.PosSemidef` `CommRing.toRing` `Matrix` `DivInvMonoid.toZPow` `Matrix.instDivInvMonoid`	—	`zpow_natCast` `pow` `Matrix.zpow_neg_natCast` `inv`

QuadraticForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`posDef_of_toMatrix'` 📖	mathematical	`Matrix.PosDef` `Real` `Real.instRing` `Real.partialOrder` `instStarRingReal` `QuadraticMap.toMatrix'` `Real.commRing` `invertibleTwo` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `IsStrictOrderedRing.toCharZero` `Real.semiring` `Real.instIsStrictOrderedRing`	`QuadraticMap.PosDef` `Real` `Real.instCommSemiring` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Pi.Function.module` `CommSemiring.toSemiring` `Semiring.toModule` `Real.partialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass` `QuadraticMap.toQuadraticMap_associated` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `LinearEquiv.left_inv` `Matrix.PosDef.toQuadraticForm'`
`posDef_toMatrix'` 📖	mathematical	`QuadraticMap.PosDef` `Real` `Real.instCommSemiring` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Pi.Function.module` `CommSemiring.toSemiring` `Semiring.toModule` `Real.partialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Matrix.PosDef` `Real` `Real.instRing` `Real.partialOrder` `instStarRingReal` `QuadraticMap.toMatrix'` `Real.commRing` `invertibleTwo` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `IsStrictOrderedRing.toCharZero` `Real.semiring` `Real.instIsStrictOrderedRing`	—	`Matrix.PosDef.of_toQuadraticForm'` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `QuadraticMap.isSymm_toMatrix'` `IsScalarTower.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `LinearMap.instSMulCommClass` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `LinearEquiv.left_inv` `QuadraticMap.toQuadraticMap_associated`

QuadraticMap

Definitions

Name	Category	Theorems
`PosDef` 📖	MathDef	17 math math: `posDef_pi_iff`, `exists_finrank_eq_sigPos_and_posDef`, `sigNeg_isGreatest`, `linMulLinSelfPosDef`, `sigPos_isGreatest`, `exists_finrank_eq_sigNeg_and_negDef`, `posDef_of_nonneg`, `IsometryEquiv.map_posDef_iff`, `posDef_prod_iff`, `Matrix.PosDef.toQuadraticForm'`, `QuadraticForm.posDef_of_toMatrix'`, `PosDef.add`, `IsometryEquiv.map_negDef_iff`, `PosDef.smul`, `posDef_iff_nonneg`, `RootPairing.posRootForm_rootFormIn_posDef`, `PosDef.prod`

---

← Back to Index