ConjTranspose

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

Statistics

Metric	Count
Definitions `conjTranspose`, `conjTransposeAddEquiv`, `conjTransposeLinearEquiv`, `conjTransposeRingEquiv`, `instInvolutiveStar`, `instStar`, `instStarAddMonoid`, `instStarRing`, `«term_ᴴ»`	9
Theorems `conjTransposeAddEquiv_apply`, `conjTransposeAddEquiv_symm`, `conjTransposeLinearEquiv_apply`, `conjTransposeLinearEquiv_symm`, `conjTransposeRingEquiv_apply`, `conjTransposeRingEquiv_symm_apply`, `conjTranspose_add`, `conjTranspose_apply`, `conjTranspose_conjTranspose`, `conjTranspose_eq_diagonal`, `conjTranspose_eq_intCast`, `conjTranspose_eq_natCast`, `conjTranspose_eq_ofNat`, `conjTranspose_eq_one`, `conjTranspose_eq_transpose_of_trivial`, `conjTranspose_eq_zero`, `conjTranspose_inj`, `conjTranspose_injective`, `conjTranspose_intCast`, `conjTranspose_intCast_smul`, `conjTranspose_inv_intCast_smul`, `conjTranspose_inv_natCast_smul`, `conjTranspose_inv_ofNat_smul`, `conjTranspose_list_prod`, `conjTranspose_list_sum`, `conjTranspose_map`, `conjTranspose_mul`, `conjTranspose_multiset_sum`, `conjTranspose_natCast`, `conjTranspose_natCast_smul`, `conjTranspose_neg`, `conjTranspose_nsmul`, `conjTranspose_ofNat`, `conjTranspose_ofNat_smul`, `conjTranspose_one`, `conjTranspose_pow`, `conjTranspose_ratCast_smul`, `conjTranspose_rat_smul`, `conjTranspose_reindex`, `conjTranspose_single`, `conjTranspose_smul`, `conjTranspose_smul_non_comm`, `conjTranspose_smul_self`, `conjTranspose_sub`, `conjTranspose_submatrix`, `conjTranspose_sum`, `conjTranspose_transpose`, `conjTranspose_vecMulVec`, `conjTranspose_zero`, `conjTranspose_zsmul`, `diag_conjTranspose`, `diagonal_conjTranspose`, `dotProduct_star`, `instStarModule`, `mulVec_conjTranspose`, `star_apply`, `star_dotProduct`, `star_dotProduct_star`, `star_eq_conjTranspose`, `star_mul`, `star_mulVec`, `star_vecMul`, `transpose_conjTranspose`, `vecMul_conjTranspose`	64
Total	73

Matrix

Definitions

Name	Category	Theorems
`conjTranspose` 📖	CompOp	158 math math: `posSemidef_conjTranspose_mul_self`, `star_eq_conjTranspose`, `isHermitian_conjTranspose_mul_mul`, `posSemidef_iff_eq_conjTranspose_mul_self`, `trace_mul_conjTranspose_self_eq_zero_iff`, `isHermitian_conjTranspose_mul_self`, `conjTranspose_sum`, `IsHermitian.conjTranspose`, `IsHermitian.fromBlocks₂₂`, `posSemidef_self_mul_conjTranspose`, `IsHermitian.eq`, `HasSum.matrix_conjTranspose`, `conjTranspose_mul_self_mulVec_eq_zero`, `conjTranspose_natCast_smul`, `isHermitian_mul_conjTranspose_self`, `PosDef.fromBlocks₁₁`, `Continuous.matrix_conjTranspose`, `conjTranspose_eq_transpose_of_trivial`, `conjTranspose_inv_intCast_smul`, `conjTranspose_natCast`, `PosSemidef.conjTranspose_mul_mul_same`, `CStarMatrix.inner_toCLM_conjTranspose_left`, `conjTranspose_sub`, `conjTranspose_eq_diagonal`, `isHermitian_conjTranspose_iff`, `ker_mulVecLin_conjTranspose_mul_self`, `conjTranspose_permMatrix`, `rank_conjTranspose`, `conjTranspose_tsum`, `PosDef.conjTranspose_mul_mul_same`, `fromBlocks_conjTranspose`, `conjTranspose_kronecker`, `star_vec_dotProduct_vec`, `conjTranspose_zero`, `star_vecMul`, `conjTranspose_inv_natCast_smul`, `eigenvalues_conjTranspose_mul_self_nonneg`, `frobenius_norm_conjTranspose`, `Fin.conjTranspose_circulant`, `IsSymm.conjTranspose`, `conjTranspose_zsmul`, `det_conjTranspose`, `conjTranspose_nonsing_inv`, `l2_opNorm_conjTranspose_mul_self`, `conjTranspose_swap`, `posDef_conjTranspose_iff`, `PosSemidef.mul_mul_conjTranspose_same`, `adjugate_conjTranspose`, `LDL.lower_conj_diag`, `l2_opNNNorm_conjTranspose`, `conjTranspose_inv_ofNat_smul`, `summable_matrix_conjTranspose`, `conjTranspose_replicateRow`, `schur_complement_eq₂₂`, `transpose_conjTranspose`, `eigenvalues_self_mul_conjTranspose_nonneg`, `blockDiagonal_conjTranspose`, `l2_opNorm_conjTranspose`, `conjTranspose_eq_natCast`, `PosDef.conjTranspose_mul_self`, `conjTranspose_submatrix`, `conjTranspose_kroneckerTMul`, `conjTranspose_ratCast_smul`, `conjTranspose_list_sum`, `exp_conjTranspose`, `conjTranspose_eq_ofNat`, `isDiag_conjTranspose_iff`, `posDef_iff_eq_conjTranspose_mul_self`, `conjTranspose_eq_intCast`, `vecMul_conjTranspose_mul_self_eq_zero`, `trace_conjTranspose_mul_self_eq_zero_iff`, `trace_conjTranspose`, `diagonal_conjTranspose`, `conjTransposeAddEquiv_apply`, `conjTranspose_fromCols_eq_fromRows_conjTranspose`, `PosSemidef.conjTranspose`, `rank_self_mul_conjTranspose`, `conjTransposeRingEquiv_symm_apply`, `conjTranspose_fromRows_eq_fromCols_conjTranspose`, `schur_complement_eq₁₁`, `conjTranspose_one`, `conjTranspose_zpow`, `PosDef.fromBlocks₂₂`, `toLin_conjTranspose`, `norm_conjTranspose`, `isHermitian_add_transpose_self`, `isUnit_conjTranspose`, `toEuclideanLin_conjTranspose_eq_adjoint`, `nnnorm_conjTranspose`, `mulVec_conjTranspose`, `conjTranspose_eq_one`, `conjTranspose_inj`, `isHermitian_fromBlocks_iff`, `isHermitian_transpose_add_self`, `vecMul_conjTranspose`, `self_mul_conjTranspose_mulVec_eq_zero`, `blockDiag'_conjTranspose`, `conjTranspose_pow`, `Summable.matrix_conjTranspose`, `IsDiag.conjTranspose`, `conjTranspose_intCast_smul`, `conjTranspose_apply`, `conjTranspose_multiset_sum`, `conjTranspose_ofNat_smul`, `updateCol_conjTranspose`, `IsHermitian.fromBlocks₁₁`, `conjTranspose_eq_zero`, `PosDef.mul_mul_conjTranspose_same`, `conjTranspose_neg`, `LDL.diag_eq_lowerInv_conj`, `conjTranspose_list_prod`, `self_mul_conjTranspose_mul_eq_zero`, `conjTranspose_smul_non_comm`, `conjTranspose_single`, `conjTranspose_vecMulVec`, `conjTranspose_transpose`, `conjTranspose_mul_self_eq_zero`, `conjTranspose_rat_smul`, `OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose`, `conjTransposeRingEquiv_apply`, `conjTranspose_smul`, `OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self`, `vecMul_self_mul_conjTranspose_eq_zero`, `isHermitian_mul_mul_conjTranspose`, `updateRow_conjTranspose`, `l2_opNNNorm_conjTranspose_mul_self`, `isHermitian_transpose_mul_self`, `inner_matrix_row_row`, `conjTranspose_mul_self_mul_eq_zero`, `conjTranspose_conjTranspose`, `conjTranspose_intCast`, `conjTranspose_smul_self`, `conjTranspose_add`, `conjTranspose_map`, `conjTranspose_kronecker'`, `LinearMap.toMatrix_adjoint`, `conjTranspose_circulant`, `self_mul_conjTranspose_eq_zero`, `conjTranspose_mul`, `conjTranspose_injective`, `posSemidef_conjTranspose_iff`, `PosDef.mul_conjTranspose_self`, `frobenius_nnnorm_conjTranspose`, `conjTranspose_ofNat`, `rank_conjTranspose_mul_self`, `PosDef.conjTranspose`, `diag_conjTranspose`, `blockDiag_conjTranspose`, `conjTranspose_replicateCol`, `blockDiagonal'_conjTranspose`, `mul_self_mul_conjTranspose_eq_zero`, `inner_matrix_col_col`, `conjTranspose_invOf`, `CStarMatrix.inner_toCLM_conjTranspose_right`, `mul_conjTranspose_mul_self_eq_zero`, `conjTranspose_nsmul`, `star_mulVec`, `conjTranspose_reindex`
`conjTransposeAddEquiv` 📖	CompOp	3 math math: `conjTransposeLinearEquiv_apply`, `conjTransposeAddEquiv_apply`, `conjTransposeAddEquiv_symm`
`conjTransposeLinearEquiv` 📖	CompOp	2 math math: `conjTransposeLinearEquiv_apply`, `conjTransposeLinearEquiv_symm`
`conjTransposeRingEquiv` 📖	CompOp	2 math math: `conjTransposeRingEquiv_symm_apply`, `conjTransposeRingEquiv_apply`
`instInvolutiveStar` 📖	CompOp	—
`instStar` 📖	CompOp	54 math math: `l2_opNorm_toEuclideanCLM`, `kroneckerTMulStarAlgEquiv_symm_apply`, `star_eq_conjTranspose`, `IsHermitian.isClosedEmbedding_cfcAux`, `IsHermitian.det_abs`, `cstar_nnnorm_def`, `IsHermitian.cfc_eq`, `instContinuousStarMatrix`, `PosSemidef.sqrt_eq_zero_iff`, `IsHermitian.isSelfAdjoint`, `LinearMap.toMatrixOrthonormal_reindex`, `IsUnit.posSemidef_star_right_conjugate_iff`, `LinearMap.toMatrixOrthonormal_apply_apply`, `toAlgEquiv_kroneckerStarAlgEquiv`, `PosSemidef.det_sqrt`, `toAlgEquiv_kroneckerTMulStarAlgEquiv`, `mem_unitaryGroup_iff`, `IsHermitian.charpoly_cfc_eq`, `PosSemidef.posSemidef_sqrt`, `toEuclideanCLM_toLp`, `PosSemidef.sqrt_eq_one_iff`, `PosSemidef.sqrt_sq`, `star_apply`, `PosSemidef.eq_sqrt_iff_sq_eq`, `isHermitian_iff_isSelfAdjoint`, `LinearMap.toMatrixOrthonormal_symm_apply`, `IsHermitian.cfcAux_apply`, `ofLp_toEuclideanCLM`, `kroneckerTMulStarAlgEquiv_apply`, `instStarModule`, `UnitaryGroup.inv_val`, `star_mul`, `PosSemidef.isUnit_sqrt_iff`, `coe_toEuclideanCLM_eq_toEuclideanLin`, `LinearMap.toMatrixOrthonormal_apply`, `PosSemidef.sq_sqrt`, `PosSemidef.inv_sqrt`, `CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv`, `IsHermitian.cfcAux_id`, `specialUnitaryGroup.coe_star`, `mem_unitaryGroup_iff'`, `IsUnit.posSemidef_star_left_conjugate_iff`, `PosSemidef.sqrt_mul_self`, `cstar_norm_def`, `UnitaryGroup.star_mul_self`, `kroneckerStarAlgEquiv_apply`, `IsUnit.posDef_star_left_conjugate_iff`, `PosDef.posDef_sqrt`, `IsHermitian.star_eigenvectorUnitary_mulVec`, `IsHermitian.instContinuousFunctionalCalculus`, `kroneckerStarAlgEquiv_symm_apply`, `PosSemidef.sqrt_eq_iff_eq_sq`, `UnitaryGroup.inv_apply`, `IsUnit.posDef_star_right_conjugate_iff`
`instStarAddMonoid` 📖	CompOp	8 math math: `kroneckerTMulStarAlgEquiv_symm_apply`, `frobenius_normedStarGroup`, `toAlgEquiv_kroneckerStarAlgEquiv`, `toAlgEquiv_kroneckerTMulStarAlgEquiv`, `kroneckerTMulStarAlgEquiv_apply`, `kroneckerStarAlgEquiv_apply`, `instNormedStarGroup`, `kroneckerStarAlgEquiv_symm_apply`
`instStarRing` 📖	CompOp	24 math math: `IsHermitian.det_abs`, `IsHermitian.cfc_eq`, `PosSemidef.sqrt_eq_zero_iff`, `PosSemidef.det_sqrt`, `IsHermitian.charpoly_cfc_eq`, `PosSemidef.posSemidef_sqrt`, `PosSemidef.sqrt_eq_one_iff`, `PosSemidef.sqrt_sq`, `PosSemidef.eq_sqrt_iff_sq_eq`, `IsHermitian.cfcAux_apply`, `UnitaryGroup.inv_val`, `PosSemidef.isUnit_sqrt_iff`, `IsHermitian.spectral_theorem`, `PosSemidef.sq_sqrt`, `PosSemidef.inv_sqrt`, `IsHermitian.star_mul_self_mul_eq_diagonal`, `instCStarRing`, `PosSemidef.sqrt_mul_self`, `instStarOrderedRing`, `IsHermitian.conjStarAlgAut_star_eigenvectorUnitary`, `PosDef.posDef_sqrt`, `IsHermitian.instContinuousFunctionalCalculus`, `PosSemidef.sqrt_eq_iff_eq_sq`, `UnitaryGroup.inv_apply`
`«term_ᴴ»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjTransposeAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Matrix` `add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `conjTransposeAddEquiv` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar`	—	—
`conjTransposeAddEquiv_symm` 📖	mathematical	—	`AddEquiv.symm` `Matrix` `add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `conjTransposeAddEquiv`	—	—
`conjTransposeLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `starRingEnd` `RingHomInvPair.instStarRingEnd` `Matrix` `addCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `conjTransposeLinearEquiv` `Equiv.toFun` `AddEquiv.toEquiv` `add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `conjTransposeAddEquiv`	—	`RingHomInvPair.instStarRingEnd`
`conjTransposeLinearEquiv_symm` 📖	mathematical	—	`LinearEquiv.symm` `Matrix` `CommSemiring.toSemiring` `addCommMonoid` `module` `starRingEnd` `RingHomInvPair.instStarRingEnd` `conjTransposeLinearEquiv`	—	`RingHomInvPair.instStarRingEnd`
`conjTransposeRingEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Matrix` `MulOpposite` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MulOpposite.instMul` `add` `Distrib.toAdd` `MulOpposite.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `conjTransposeRingEquiv` `MulOpposite.op` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	—
`conjTransposeRingEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MulOpposite` `Matrix` `MulOpposite.instMul` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MulOpposite.instAdd` `add` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `conjTransposeRingEquiv` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `MulOpposite.unop`	—	—
`conjTranspose_add` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `Matrix` `add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`ext` `StarAddMonoid.star_add`
`conjTranspose_apply` 📖	mathematical	—	`conjTranspose` `Star.star`	—	—
`conjTranspose_conjTranspose` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar`	—	`ext` `star_star`
`conjTranspose_eq_diagonal` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `diagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Star.star` `Pi.instStarForall`	—	`Function.Involutive.eq_iff` `conjTranspose_conjTranspose` `diagonal_conjTranspose`
`conjTranspose_eq_intCast` 📖	mathematical	—	`conjTranspose` `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`	—	`Function.Involutive.eq_iff` `conjTranspose_conjTranspose` `conjTranspose_intCast`
`conjTranspose_eq_natCast` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Function.Involutive.eq_iff` `conjTranspose_conjTranspose` `conjTranspose_natCast`
`conjTranspose_eq_ofNat` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instOfNatAtLeastTwo` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`conjTranspose_eq_natCast`
`conjTranspose_eq_one` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Function.Involutive.eq_iff` `conjTranspose_conjTranspose` `conjTranspose_one`
`conjTranspose_eq_transpose_of_trivial` 📖	mathematical	—	`conjTranspose` `transpose`	—	`ext` `TrivialStar.star_trivial`
`conjTranspose_eq_zero` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `Matrix` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`conjTranspose_zero`
`conjTranspose_inj` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar`	—	`conjTranspose_injective`
`conjTranspose_injective` 📖	mathematical	—	`Matrix` `conjTranspose` `InvolutiveStar.toStar`	—	`map_injective` `star_injective` `transpose_injective`
`conjTranspose_intCast` 📖	mathematical	—	`conjTranspose` `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`	—	`transpose_intCast` `map_intCast` `star_zero` `star_intCast`
`conjTranspose_intCast_smul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`ext` `star_intCast_smul`
`conjTranspose_inv_intCast_smul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`ext` `star_inv_intCast_smul`
`conjTranspose_inv_natCast_smul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Module.toDistribMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`ext` `star_inv_natCast_smul`
`conjTranspose_inv_ofNat_smul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Module.toDistribMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`conjTranspose_inv_natCast_smul`
`conjTranspose_list_prod` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingEquiv.unop_map_list_prod`
`conjTranspose_list_sum` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `Matrix` `add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`map_list_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`conjTranspose_map` 📖	mathematical	`Function.Semiconj` `Star.star`	`map` `conjTranspose`	—	`ext`
`conjTranspose_mul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`ext` `star_sum` `Finset.sum_congr` `StarMul.star_mul`
`conjTranspose_multiset_sum` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Multiset.sum` `Matrix` `addCommMonoid` `Multiset.map`	—	`AddMonoidHom.map_multiset_sum`
`conjTranspose_natCast` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`transpose_natCast` `map_natCast` `star_zero` `star_natCast`
`conjTranspose_natCast_smul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`ext` `star_natCast_smul`
`conjTranspose_neg` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Matrix` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ext` `star_neg`
`conjTranspose_nsmul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `Matrix` `AddMonoid.toNatSMul` `addMonoid`	—	`ext` `star_nsmul`
`conjTranspose_ofNat` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `instOfNatAtLeastTwo` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`conjTranspose_natCast`
`conjTranspose_ofNat_smul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`conjTranspose_natCast_smul`
`conjTranspose_one` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`transpose_one` `map_one` `star_zero` `star_one`
`conjTranspose_pow` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`MulOpposite.op_injective` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`
`conjTranspose_ratCast_smul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `DivisionRing.toRatCast`	—	`ext` `star_ratCast_smul`
`conjTranspose_rat_smul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Rat.monoid` `Module.toDistribMulAction` `Rat.semiring` `AddCommGroup.toAddCommMonoid`	—	`ext` `star_rat_smul`
`conjTranspose_reindex` 📖	mathematical	—	`conjTranspose` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex`	—	—
`conjTranspose_single` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Star.star`	—	`transpose_single` `map_single` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`conjTranspose_smul` 📖	mathematical	—	`conjTranspose` `Matrix` `smul` `Star.star`	—	`ext` `StarModule.star_smul`
`conjTranspose_smul_non_comm` 📖	mathematical	`Star.star` `MulOpposite` `MulOpposite.op`	`conjTranspose` `Matrix` `smul`	—	`ext`
`conjTranspose_smul_self` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `Matrix` `smul` `MulOpposite` `Mul.toSMulMulOpposite` `MulOpposite.op` `Star.star`	—	`conjTranspose_smul_non_comm` `StarMul.star_mul`
`conjTranspose_sub` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Matrix` `sub` `SubNegMonoid.toSub`	—	`ext` `star_sub`
`conjTranspose_submatrix` 📖	mathematical	—	`conjTranspose` `submatrix`	—	`ext`
`conjTranspose_sum` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `Finset.sum` `Matrix` `addCommMonoid`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`conjTranspose_transpose` 📖	mathematical	—	`transpose` `conjTranspose` `map` `Star.star`	—	—
`conjTranspose_vecMulVec` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `vecMulVec` `Star.star` `Pi.instStarForall`	—	`ext` `StarMul.star_mul`
`conjTranspose_zero` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `Matrix` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`ext` `star_zero`
`conjTranspose_zsmul` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Matrix` `SubNegMonoid.toZSMul` `addGroup`	—	`ext` `star_zsmul`
`diag_conjTranspose` 📖	mathematical	—	`diag` `conjTranspose` `Star.star` `Pi.instStarForall`	—	—
`diagonal_conjTranspose` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `diagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Star.star` `Pi.instStarForall`	—	`conjTranspose.eq_1` `diagonal_transpose` `diagonal_map` `star_zero`
`dotProduct_star` 📖	mathematical	—	`dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`Finset.sum_congr` `star_sum` `StarMul.star_mul` `star_star`
`instStarModule` 📖	mathematical	—	`StarModule` `Matrix` `instStar` `smul`	—	`conjTranspose_smul`
`mulVec_conjTranspose` 📖	mathematical	—	`mulVec` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `Star.star` `Pi.instStarForall` `vecMul`	—	`star_dotProduct`
`star_apply` 📖	mathematical	—	`Star.star` `Matrix` `instStar`	—	—
`star_dotProduct` 📖	mathematical	—	`dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`Finset.sum_congr` `star_sum` `StarMul.star_mul` `star_star`
`star_dotProduct_star` 📖	mathematical	—	`dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid`	—	`Finset.sum_congr` `star_sum` `StarMul.star_mul`
`star_eq_conjTranspose` 📖	mathematical	—	`Star.star` `Matrix` `instStar` `conjTranspose`	—	—
`star_mul` 📖	mathematical	—	`Star.star` `Matrix` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`conjTranspose_mul`
`star_mulVec` 📖	mathematical	—	`Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `mulVec` `vecMul` `conjTranspose`	—	`star_dotProduct_star`
`star_vecMul` 📖	mathematical	—	`Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `vecMul` `mulVec` `conjTranspose`	—	`star_dotProduct_star`
`transpose_conjTranspose` 📖	mathematical	—	`conjTranspose` `transpose` `map` `Star.star`	—	—
`vecMul_conjTranspose` 📖	mathematical	—	`vecMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `Star.star` `Pi.instStarForall` `mulVec`	—	`dotProduct_star`

---

← Back to Index