Hermitian

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

Statistics

Metric	Count
Definitions `IsHermitian`, `instDecidableIsHermitianOfEqConjTranspose`, `«term_⊕ᵥ_»`	3
Theorems `isHermitian`, `add`, `adjugate`, `apply`, `commute_iff`, `conjTranspose`, `eq`, `ext`, `ext_iff`, `fromBlocks`, `fromBlocks₁₁`, `fromBlocks₂₂`, `inv`, `isSelfAdjoint`, `map`, `neg`, `of_smul`, `of_smul'`, `of_subsingleton`, `pow`, `reindex`, `smul`, `sub`, `submatrix`, `transpose`, `zpow`, `conjTranspose_comp`, `conjTranspose_comp'`, `isHermitian_add_transpose_self`, `isHermitian_comp_iff`, `isHermitian_comp_iff_forall`, `isHermitian_conjTranspose_iff`, `isHermitian_conjTranspose_mul_mul`, `isHermitian_conjTranspose_mul_self`, `isHermitian_diagonal`, `isHermitian_diagonal_iff`, `isHermitian_diagonal_of_self_adjoint`, `isHermitian_fromBlocks_iff`, `isHermitian_iff_isSelfAdjoint`, `isHermitian_intCast`, `isHermitian_inv`, `isHermitian_map_iff`, `isHermitian_mul_conjTranspose_self`, `isHermitian_mul_mul_conjTranspose`, `isHermitian_natCast`, `isHermitian_neg_iff`, `isHermitian_one`, `isHermitian_reindex_iff`, `isHermitian_smul_iff`, `isHermitian_submatrix_equiv`, `isHermitian_transpose_add_self`, `isHermitian_transpose_iff`, `isHermitian_transpose_mul_self`, `isHermitian_zero`, `schur_complement_eq₁₁`, `schur_complement_eq₂₂`	56
Total	59

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isHermitian` 📖	mathematical	`IsSelfAdjoint` `Matrix` `Matrix.instStar`	`Matrix.IsHermitian`	—	`Matrix.isHermitian_iff_isSelfAdjoint`

Matrix

Definitions

Name	Category	Theorems
`IsHermitian` 📖	MathDef	69 math math: `isHermitian_conjTranspose_mul_mul`, `IsHermitian.zpow`, `isHermitian_conjTranspose_mul_self`, `IsHermitian.conjTranspose`, `IsHermitian.fromBlocks₂₂`, `PosSemidef.isHermitian`, `isHermitian_comp_iff_forall`, `posDef_iff_dotProduct_mulVec`, `PosDef.eigenvalues_pos`, `isHermitian_mul_conjTranspose_self`, `IsHermitian.add`, `LinearMap.isHermitian_toMatrix_iff`, `SimpleGraph.isHermitian_adjMatrix`, `IsHermitian.neg`, `IsHermitian.of_smul'`, `isHermitian_conjTranspose_iff`, `IsHermitian.ext_iff`, `IsHermitian.transpose`, `RKHS.isHermitian_kernel`, `RKHS.posSemidef_tfae`, `IsHermitian.exp`, `isSymmetric_toEuclideanLin_iff`, `isHermitian_comp_iff`, `isHermitian_map_iff`, `PosSemidef.eigenvalues_nonneg`, `IsSelfAdjoint.isHermitian`, `isHermitian_iff_isSelfAdjoint`, `isHermitian_reindex_iff`, `isHermitian_gram`, `IsHermitian.ext`, `isHermitian_inv`, `IsHermitian.of_smul`, `IsHermitian.commute_iff`, `IsHermitian.reindex`, `IsHermitian.map`, `isHermitian_submatrix_equiv`, `IsHermitian.inv`, `isHermitian_add_transpose_self`, `isHermitian_iff_isSymmetric`, `SimpleGraph.isHermitian_lapMatrix`, `SimpleGraph.isHermitian_degMatrix`, `isSymmetric_toLin_iff`, `isHermitian_fromBlocks_iff`, `isHermitian_transpose_add_self`, `isHermitian_natCast`, `IsHermitian.smul`, `posSemidef_iff_dotProduct_mulVec`, `IsHermitian.pow`, `IsHermitian.of_subsingleton`, `IsHermitian.fromBlocks₁₁`, `isHermitian_zero`, `IsAdjMatrix.isHermitian`, `isHermitian_one`, `IsHermitian.submatrix`, `IsHermitian.adjugate`, `isHermitian_smul_iff`, `isHermitian_diagonal_iff`, `isHermitian_mul_mul_conjTranspose`, `IsHermitian.sub`, `isHermitian_diagonal_of_self_adjoint`, `isHermitian_transpose_mul_self`, `isHermitian_diagonal`, `IsHermitian.fromBlocks`, `isHermitian_intCast`, `isHermitian_neg_iff`, `isHermitian_transpose_iff`, `posSemidef_iff_isHermitian_and_spectrum_nonneg`, `PosDef.isHermitian`, `LinearMap.isSymm_iff_isHermitian_toMatrix`
`instDecidableIsHermitianOfEqConjTranspose` 📖	CompOp	—
`«term_⊕ᵥ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjTranspose_comp` 📖	mathematical	—	`conjTranspose` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `map` `transpose`	—	—
`conjTranspose_comp'` 📖	mathematical	—	`conjTranspose` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `instStar`	—	—
`isHermitian_add_transpose_self` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Matrix` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `conjTranspose`	—	`IsSelfAdjoint.add_star_self`
`isHermitian_comp_iff` 📖	mathematical	—	`IsHermitian` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `instStar`	—	`IsHermitian.eq_1` `conjTranspose_comp'` `Equiv.injective`
`isHermitian_comp_iff_forall` 📖	mathematical	—	`IsHermitian` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `Star.star`	—	—
`isHermitian_conjTranspose_iff` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `conjTranspose`	—	`IsSelfAdjoint.star_iff`
`isHermitian_conjTranspose_mul_mul` 📖	mathematical	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `conjTranspose`	—	`mul_assoc` `conjTranspose_mul` `IsHermitian.eq` `conjTranspose_conjTranspose`
`isHermitian_conjTranspose_mul_self` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `conjTranspose`	—	`IsHermitian.eq_1` `conjTranspose_mul` `conjTranspose_conjTranspose`
`isHermitian_diagonal` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `diagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`isHermitian_diagonal_of_self_adjoint` `IsSelfAdjoint.all` `Pi.instTrivialStarForall`
`isHermitian_diagonal_iff` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `diagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `IsSelfAdjoint`	—	`diagonal_transpose` `diagonal_map` `star_zero`
`isHermitian_diagonal_of_self_adjoint` 📖	mathematical	`IsSelfAdjoint` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar`	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `diagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`diagonal_conjTranspose`
`isHermitian_fromBlocks_iff` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `fromBlocks` `conjTranspose`	—	`IsHermitian.fromBlocks`
`isHermitian_iff_isSelfAdjoint` 📖	mathematical	—	`IsHermitian` `IsSelfAdjoint` `Matrix` `instStar`	—	—
`isHermitian_intCast` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `StarRing.toStarAddMonoid` `Matrix` `instIntCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`conjTranspose_intCast`
`isHermitian_inv` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid` `Matrix` `inv`	—	`inv_inv_of_invertible` `IsHermitian.inv`
`isHermitian_map_iff` 📖	mathematical	`Function.Semiconj` `Star.star`	`IsHermitian` `map`	—	`IsHermitian.eq_1` `conjTranspose_map` `map_injective`
`isHermitian_mul_conjTranspose_self` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `conjTranspose`	—	`IsHermitian.eq_1` `conjTranspose_mul` `conjTranspose_conjTranspose`
`isHermitian_mul_mul_conjTranspose` 📖	mathematical	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `conjTranspose`	—	`mul_assoc` `conjTranspose_mul` `conjTranspose_conjTranspose` `IsHermitian.eq`
`isHermitian_natCast` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`conjTranspose_natCast`
`isHermitian_neg_iff` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Matrix` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`neg_neg` `IsHermitian.neg`
`isHermitian_one` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`conjTranspose_one`
`isHermitian_reindex_iff` 📖	mathematical	—	`IsHermitian` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex`	—	`submatrix_submatrix` `Equiv.symm_comp_self` `submatrix_id_id` `IsHermitian.reindex`
`isHermitian_smul_iff` 📖	mathematical	`IsSelfAdjoint`	`IsHermitian` `Matrix` `smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`IsHermitian.of_smul` `IsHermitian.smul`
`isHermitian_submatrix_equiv` 📖	mathematical	—	`IsHermitian` `submatrix` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`submatrix_submatrix` `Equiv.self_comp_symm` `submatrix_id_id` `IsHermitian.submatrix`
`isHermitian_transpose_add_self` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Matrix` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `conjTranspose`	—	`IsSelfAdjoint.star_add_self`
`isHermitian_transpose_iff` 📖	mathematical	—	`IsHermitian` `transpose`	—	`transpose_transpose` `IsHermitian.transpose`
`isHermitian_transpose_mul_self` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `conjTranspose`	—	`isHermitian_conjTranspose_mul_self`
`isHermitian_zero` 📖	mathematical	—	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `Matrix` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`IsSelfAdjoint.zero`
`schur_complement_eq₁₁` 📖	mathematical	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	`dotProduct` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `vecMul` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `fromBlocks` `conjTranspose` `Distrib.toAdd` `Pi.instAdd` `mulVec` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `inv` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Function.star_sumElim` `vecMul_fromBlocks` `sumElim_dotProduct_sumElim` `add_dotProduct` `StarAddMonoid.star_add` `star_mulVec` `conjTranspose_mul` `conjTranspose_nonsing_inv` `IsHermitian.eq` `add_vecMul` `vecMul_vecMul` `mul_assoc` `inv_mul_of_invertible` `mul_one` `dotProduct_add` `dotProduct_mulVec` `mul_inv_cancel_left_of_invertible` `vecMul_sub` `sub_dotProduct` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.const_add_termg` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg`
`schur_complement_eq₂₂` 📖	mathematical	`IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	`dotProduct` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `vecMul` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `fromBlocks` `conjTranspose` `Distrib.toAdd` `Pi.instAdd` `mulVec` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `inv` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Function.star_sumElim` `vecMul_fromBlocks` `sumElim_dotProduct_sumElim` `add_dotProduct` `StarAddMonoid.star_add` `star_mulVec` `conjTranspose_mul` `conjTranspose_conjTranspose` `conjTranspose_nonsing_inv` `IsHermitian.eq` `add_vecMul` `vecMul_vecMul` `mul_assoc` `inv_mul_of_invertible` `mul_one` `dotProduct_add` `dotProduct_mulVec` `mul_inv_cancel_left_of_invertible` `vecMul_sub` `sub_dotProduct` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg`

Matrix.IsHermitian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `Matrix` `Matrix.add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`IsSelfAdjoint.add`
`adjugate` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid` `Matrix.adjugate`	—	`Matrix.adjugate_conjTranspose` `eq`
`apply` 📖	mathematical	`Matrix.IsHermitian`	`Star.star`	—	—
`commute_iff` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	`Commute` `Matrix` `Matrix.instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid`	—	`IsSelfAdjoint.commute_iff` `isSelfAdjoint`
`conjTranspose` 📖	mathematical	`Matrix.IsHermitian`	`Matrix.IsHermitian` `Matrix.conjTranspose`	—	`map` `transpose`
`eq` 📖	mathematical	`Matrix.IsHermitian`	`Matrix.conjTranspose`	—	—
`ext` 📖	mathematical	`Star.star`	`Matrix.IsHermitian`	—	`Matrix.ext`
`ext_iff` 📖	mathematical	—	`Matrix.IsHermitian` `Star.star`	—	`apply` `ext`
`fromBlocks` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `Matrix.conjTranspose`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `Matrix.fromBlocks`	—	`Matrix.conjTranspose_conjTranspose` `Matrix.fromBlocks_conjTranspose`
`fromBlocks₁₁` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid` `Matrix.fromBlocks` `Matrix.conjTranspose` `Matrix` `Matrix.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Matrix.inv`	—	`Matrix.isHermitian_conjTranspose_mul_mul` `inv` `Matrix.isHermitian_fromBlocks_iff` `sub` `Matrix.conjTranspose_conjTranspose` `add` `sub_add_cancel`
`fromBlocks₂₂` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid` `Matrix.fromBlocks` `Matrix.conjTranspose` `Matrix` `Matrix.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Matrix.inv`	—	`Matrix.isHermitian_submatrix_equiv` `Equiv.sumComm_apply` `Matrix.fromBlocks_submatrix_sum_swap_sum_swap` `Matrix.conjTranspose_conjTranspose` `fromBlocks₁₁`
`inv` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid` `Matrix` `Matrix.inv`	—	`Matrix.conjTranspose_nonsing_inv` `eq`
`isSelfAdjoint` 📖	mathematical	`Matrix.IsHermitian`	`IsSelfAdjoint` `Matrix` `Matrix.instStar`	—	`Matrix.isHermitian_iff_isSelfAdjoint`
`map` 📖	mathematical	`Matrix.IsHermitian` `Function.Semiconj` `Star.star`	`Matrix.IsHermitian` `Matrix.map`	—	`eq_1` `Matrix.conjTranspose_map` `eq`
`neg` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Matrix` `Matrix.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`IsSelfAdjoint.neg`
`of_smul` 📖	mathematical	`Matrix.IsHermitian` `Matrix` `Matrix.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `IsSelfAdjoint`	`Matrix.IsHermitian`	—	`invOf_smul_smul` `IsSelfAdjoint.star_eq` `Matrix.conjTranspose_smul` `eq_1`
`of_smul'` 📖	mathematical	`Matrix.IsHermitian` `Matrix` `Matrix.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `IsSelfAdjoint` `Invertible.invOf` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	`Matrix.IsHermitian`	—	`invOf_smul_smul` `smul`
`of_subsingleton` 📖	mathematical	—	`Matrix.IsHermitian`	—	`ext`
`pow` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring`	—	`IsSelfAdjoint.pow`
`reindex` 📖	mathematical	`Matrix.IsHermitian`	`Matrix.IsHermitian` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.reindex`	—	`Matrix.reindex_apply` `submatrix`
`smul` 📖	mathematical	`Matrix.IsHermitian` `IsSelfAdjoint`	`Matrix.IsHermitian` `Matrix` `Matrix.smul`	—	`eq_1` `Matrix.conjTranspose_smul` `IsSelfAdjoint.star_eq` `eq`
`sub` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Matrix` `Matrix.sub` `SubNegMonoid.toSub`	—	`IsSelfAdjoint.sub`
`submatrix` 📖	mathematical	`Matrix.IsHermitian`	`Matrix.IsHermitian` `Matrix.submatrix`	—	`Matrix.conjTranspose_submatrix`
`transpose` 📖	mathematical	`Matrix.IsHermitian`	`Matrix.IsHermitian` `Matrix.transpose`	—	`eq_1` `Matrix.conjTranspose.eq_1` `Matrix.transpose_map`
`zpow` 📖	mathematical	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid`	`Matrix.IsHermitian` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `StarRing.toStarAddMonoid` `Matrix` `DivInvMonoid.toZPow` `Matrix.instDivInvMonoid`	—	`eq_1` `Matrix.conjTranspose_zpow`

---

← Back to Index