| Name | Category | Theorems |
|---|
diag π | CompOp | 41 mathmath: diag_smul, hadamard_one_eq_zero_iff, diag_zero, diag_vecMulVec, hadamard_diagonal_eq_diagonal_iff, diag_replicateCol_mul_replicateRow, hadamard_one, diag_diagonal, one_hadamard_eq_diagonal_iff, diag_multiset_sum, diag_transpose, HasSum.matrix_diag, IsDiag.diagonal_diag, Summable.matrix_diag, hadamard_one_eq_one_iff, one_hadamard_eq_one_iff, diag_apply, one_hadamard, diagAddMonoidHom_apply, diag_submatrix, continuous_matrix_diag, one_hadamard_eq_zero_iff, diagonal_hadamard, diag_map, diag_add, diag_single_same, diag_neg, Continuous.matrix_diag, IsHermitian.coe_re_diag, diag_one, diagonal_hadamard_eq_diagonal_iff, diag_list_sum, isDiag_iff_diagonal_diag, diag_sum, hadamard_diagonal, LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, CartanMatrix.A_diag, diag_single_of_ne, hadamard_one_eq_diagonal_iff, diag_conjTranspose, diag_sub
|
diagonal π | CompOp | 188 mathmath: comp_diagonal_diagonal, RootPairing.GeckConstruction.h_def, linfty_opNorm_diagonal, norm_diagonal, toBlock_diagonal_disjoint, diagonal_natCast, submatrix_diagonal, diagonal_mem_matrix_iff, iSup_eigenspace_toLin'_diagonal_eq_top, diagonal_vec3, diagonal_fin_two, blockDiag'_diagonal, diagonal_eq_diagonal_iff, diagonal_natCast', toMatrix_distrib_mul_action_toLinearMap, blockTriangular_diagonal, diagonal_vec1, diagonal_pow, smul_one_eq_diagonal, Real.smul_map_diagonal_volume_pi, matPolyEquiv_diagonal_X, IsHermitian.rank_eq_rank_diagonal, spectrum_diagonal, diagonal_updateRow_single, diagonal_one', LinearMap.rank_diagonal, op_smul_one_eq_diagonal, hadamard_diagonal_eq_diagonal_iff, vecMul_diagonal, conjTranspose_eq_diagonal, diagonal_zero, diagonal_vec2, diagonal_apply_ne', hadamard_one, diagonal_ofNat', diagonal_apply_eq, transpose_eq_diagonal, summable_matrix_diagonal, diagonal_smul, diag_diagonal, PosSemidef.diagonal, trace_diagonal, row_diagonal, blockDiagonal'_diagonal, Summable.matrix_diagonal, exp_diagonal, Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux, toBlocksββ_diagonal, l2_opNorm_diagonal, kroneckerMap_diagonal_right, diagonal_ofNat, cRank_diagonal, hasEigenvector_toLin'_diagonal, one_hadamard_eq_diagonal_iff, op_smul_eq_mul_diagonal, diagonal_updateCol_single, eRank_diagonal, diagonal_dotProduct, IsDiag.diagonal_diag, IsHermitian.cfcAux_apply, diagonal_kroneckerTMul_diagonal, diagonal_kroneckerTMul, HasSum.matrix_diagonal, diagonal_fin_one, det_diagonal, diagonal_injective, adjugate_diagonal, diagonal_mul, smul_eq_mul_diagonal, charmatrix_natCast, diagonal_toLin', Polynomial.sylvester_zero_left_deg, permanent_diagonal, one_hadamard, fromBlocks_diagonal, diagonal_conjTranspose, diagonalAddMonoidHom_apply, algebraMap_eq_diagonal, toBlocksββ_diagonal, blockDiag_diagonal, ker_diagonal_toLin', submatrix_diagonal_equiv, diagonal_mul_diagonal', frobenius_nnnorm_diagonal, comp_symm_diagonal, IsHermitian.spectral_theorem, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, diagonalAlgHom_apply, diagonal_mulVec_single, toBlock_diagonal_self, diagonal_hadamard, diagonal_sub, toBlocksββ_diagonal, vecMul_diagonal_const, map_natCast, rank_diagonal, diagonal_one, diagonal_transpose, diagonal_kronecker, blockDiagonal_diagonal, diagonalRingHom_apply, invOf_diagonal_eq, dotProduct_vecMul_hadamard, proj_diagonal, Continuous.matrix_diagonal, col_diagonal, Algebra.toMatrix_lsmul, diagonal_apply, charmatrix_one, GeneralLinearGroup.val_inv_scalar_apply, diagonalInvertibleEquivInvertible_symm_apply, kroneckerMap_diagonal_diagonal, diagonal_kronecker_diagonal, submatrix_diagonal_embedding, Module.Basis.toMatrix_isUnitSMul, diagonal_hadamard_diagonal, hasEigenvalue_toLin'_diagonal_iff, diagonal_add, map_intCast, diagonalInvertibleEquivInvertible_apply, diagonal_hadamard_eq_diagonal_iff, Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal, diagonal_const_mulVec, posSemidef_diagonal_iff, kroneckerTMul_diagonal, frobenius_norm_diagonal, commute_diagonal, diagonal_neg, Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec, isDiag_diagonal, PosDef.diagonal, diagonal_unique, nnnorm_diagonal, sum_single_eq_diagonal, diagonal_mul_diagonal, Module.diagonal_const_smul, IsHermitian.star_mul_self_mul_eq_diagonal, l2_opNNNorm_diagonal, matPolyEquiv_symm_X, comp_diagonal, isDiag_iff_diagonal_diag, charmatrix_apply, map_ofNat, charmatrix_ofNat, diagonal_single, scalar_apply, isHermitian_diagonal_iff, range_diagonal, dotProduct_diagonal', RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, maxGenEigenspace_toLin_diagonal_eq_eigenspace, hadamard_diagonal, diagonal_tsum, Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix, mulVec_diagonal, isHermitian_diagonal_of_self_adjoint, diagonal_map, diagonal_fin_three, iSup_eigenspace_toLin_diagonal_eq_top, GeneralLinearGroup.val_scalar_apply, maxGenEigenspace_toLin'_diagonal_eq_eigenspace, isHermitian_diagonal, isUnit_diagonal, IsHermitian.conjStarAlgAut_star_eigenvectorUnitary, RootPairing.GeckConstruction.h_eq_diagonal, charpoly_diagonal, mul_diagonal, inv_subsingleton, smul_eq_diagonal_mul, diagonal_intCast', dotProduct_diagonal, Module.Basis.toMatrix_unitsSMul, charmatrix_diagonal, diagonal_zero', linfty_opNNNorm_diagonal, hasEigenvector_toLin_diagonal, diagonal_comp_single, diagonal_apply_ne, single_vecMul_diagonal, inv_diagonal, isSymm_diagonal, kronecker_diagonal, kroneckerMap_diagonal_left, posDef_diagonal_iff, hadamard_one_eq_diagonal_iff, toBlocksββ_diagonal, diagonal_intCast, hasEigenvalue_toLin_diagonal_iff
|
instAddCommGroupWithOne π | CompOp | β |
instAddCommMonoidWithOne π | CompOp | 1 mathmath: kroneckerTMulLinearEquiv_one
|
instAddGroupWithOne π | CompOp | β |
instAddMonoidWithOne π | CompOp | 1 mathmath: charP
|
instIntCastOfZero π | CompOp | 18 mathmath: transpose_eq_intCast, PosSemidef.intCast, conjTranspose_eq_intCast, transpose_intCast, den_intCast, posSemidef_intCast_iff, sum_single_intCast, map_intCast, posDef_intCast_iff, num_intCast, intCast_apply, PosDef.intCast, intCast_mulVec, conjTranspose_intCast, isHermitian_intCast, vecMul_intCast, diagonal_intCast', diagonal_intCast
|
instNatCastOfZero π | CompOp | 32 mathmath: natCast_kronecker, kronecker_natCast, diagonal_natCast, transpose_ofNat, natCast_apply, RootPairing.Base.cartanMatrix_map_abs, diagonal_natCast', PosSemidef.natCast, charpoly_natCast, conjTranspose_natCast, diagonal_ofNat', natCast_fin_three, PosDef.natCast, transpose_eq_ofNat, natCast_fin_two, diagonal_ofNat, conjTranspose_eq_natCast, transpose_natCast, conjTranspose_eq_ofNat, charmatrix_natCast, num_ofNat, num_natCast, map_natCast, isHermitian_natCast, vecMul_natCast, posDef_natCast_iff, natCast_mulVec, sum_single_natCast, natCast_kronecker_natCast, den_natCast, conjTranspose_ofNat, transpose_eq_natCast
|
one π | CompOp | 263 mathmath: toBlock_one_disjoint, toLinAlgEquiv_one, list_prod_inv_reverse, swap_mul_self, invOf_fromBlocksββ_eq, transposeInvertibleEquivInvertible_symm_apply, Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col, add_mul_mul_invOf_mul_eq_one, one_div_pow, det_add_replicateCol_mul_replicateRow, one_kronecker, Pivot.listTransvecCol_mul_last_col, hadamard_one_eq_zero_iff, mul_invOf_eq_iff_eq_mul_right, Polynomial.leadingCoeff_det_X_one_add_C, LinearMap.toMatrix_one, sum_single_one, detp_neg_one_one, mulRightLinearMap_one, exists_right_inverse_iff_isUnit, zero_le_one_elem, blockDiag_one, SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, toMvPolynomial_one, smul_one_eq_diagonal, isDiag_one, rank_one, fromBlocks_eq_of_invertibleββ, one_apply, derivative_det_one_add_X_smul, transpose_eq_one, diagonal_one', LinearMap.toMatrixAlgEquiv'_id, op_smul_one_eq_diagonal, updateRow_eq_transvection, mul_inv_of_invertible, AffineBasis.toMatrix_mul_toMatrix, SpecialLinearGroup.coe_one, det_add_mul, blockDiagonal'_one, LieAlgebra.Orthogonal.jb_transform, PosSemidef.one, TensorProduct.toMatrix_assoc, Pivot.mul_listTransvecRow_last_col, det_one_add_smul, LinearMap.toMatrix_id, mul_reindexLinearEquiv_one, CategoryTheory.HomOrthogonal.matrixDecomposition_id, LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, frobenius_nnnorm_one, adjugate_fin_one, one_apply_ne, PEquiv.toMatrix_toPEquiv_eq, mem_unitaryGroup_iff, one_eq_pi_single, hadamard_one, one_fromCols_isTotallyUnimodular_iff, toLinearEquiv'_symm_apply, LinearMap.toMatrixAlgEquiv_id, permanent_one, Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec, one_fromRows_isTotallyUnimodular_iff, TransvectionStruct.det_toMatrix_prod, detp_one_one, PosSemidef.sqrt_eq_one_iff, toLpLin_one, invOf_eq_nonsing_inv, equiv_compl_fromCols_mul_fromRows_eq_one_comm, TransvectionStruct.inv_mul, kroneckerMap_one_one, TransvectionStruct.toMatrix_reindexEquiv_prod, invOf_mul_eq_iff_eq_mul_left, Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux, one_zpow, map_one, J_squared, nonsing_inv_mul, eRank_one, GeneralLinearGroup.coe_one, IsTotallyUnimodular.fromCols_one, circulant_single_one, PosDef.one, UnitaryGroup.one_apply, mulVecLin_one, reindexLinearEquiv_one, kroneckerTMulLinearEquiv_one, transvection_zero, one_hadamard_eq_diagonal_iff, IsTotallyUnimodular.one_fromRows, UnitaryGroup.one_val, TransvectionStruct.prod_mul_reverse_inv_prod, SimpleGraph.IsSRGWith.matrix_eq, adjugate_eq_one_of_card_eq_one, blockDiag'_one, charpoly_one, det_one_add_X_smul, TransvectionStruct.mul_sumInl_toMatrix_prod, permMatrix_one, det_one_sub_mul_comm, add_mul_mul_invOf_mul_eq_one', mul_eq_one_comm_of_card_eq, instNormOneClassOfNonempty, fromRows_one_isTotallyUnimodular_iff, det_fromBlocksββ, toLpLin_symm_id, add_mul_mul_mul_invOf_eq_one, det_fromBlocks_oneββ, hadamard_one_eq_one_iff, one_hadamard_eq_one_iff, invOf_fromBlocks_zeroββ_eq, transpose_invOf, one_submatrix_mul, one_apply_ne', LieAlgebra.Orthogonal.s_as_blocks, one_hadamard, isUnit_fromBlocks_iff_of_invertibleββ, BlockTriangular.toBlock_inverse_mul_toBlock_eq_one, mul_invOf_cancel_right, cRank_one, fromBlocks_eq_of_invertibleββ, LinearMap.toMatrixRight'_id, invOf_add_mul_mul, Pivot.mul_listTransvecRow_last_row, conjTranspose_one, MatrixEquivTensor.invFun_smul, submatrix_one, det_fromBlocks_oneββ, kronecker_one, SymplecticGroup.inv_left_mul_aux, isUnit_fromBlocks_iff_of_invertibleββ, exists_left_inverse_iff_isUnit, toLin'_one, vecMul_surjective_iff_exists_left_inverse, fromBlocks_one, zero_le_one_row, one_hadamard_eq_zero_iff, one_kronecker_one, submatrix_one_equiv, mul_submatrix_one, Pivot.listTransvecCol_mul_last_row_drop, add_mul_mul_mul_invOf_eq_one', nonsing_inv_cancel_or_zero, Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row, Module.Basis.toMatrix_mul_toMatrix_flip, mul_right_eq_iff_eq_mul_invOf, diagonal_one, LinearMap.toMatrix'_id, submatrix_one_embedding, conjTranspose_eq_one, RootPairing.GeckConstruction.Ο_mul_Ο, transpose_one, invOf_diagonal_eq, mem_orthogonalGroup_iff, inv_mul_of_invertible, Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow, det_fromBlocksββ, mul_left_eq_iff_eq_invOf_mul, fromCols_mul_fromRows_eq_one_comm, Pivot.mul_listTransvecRow_last_col_take, Pivot.exists_isTwoBlockDiagonal_of_ne_zero, mulLeftLinearMap_one, GeneralLinearGroup.coe_map_mul_map_inv, det_mul_add_one_comm, linfty_opNormOneClass, isDiag_smul_one, submatrixEquivInvertibleEquivInvertible_apply, charmatrix_one, coeff_det_one_add_X_smul_one, Pivot.listTransvecCol_mul_last_row, mul_eq_one_comm_of_equiv, isAdjMatrix_iff_hadamard, num_one, diagonalInvertibleEquivInvertible_symm_apply, Represents.one, one_fin_three, trace_one, invOf_mul_cancel_right, toBlock_one_self, mul_invOf_cancel_left, diag_one, mem_unitaryGroup_iff', diagonalInvertibleEquivInvertible_apply, invertibleEquivDetInvertible_apply, adjugate_subsingleton, Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal, invOf_add_mul_mul', Algebra.Norm.Transitivity.mul_auxMat_toSquareBlock_eq, cramer_one, det_one, adjugate_one, conjTranspose_list_prod, toLinAlgEquiv'_one, toLin_one, invOf_fromBlocks_zeroββ_eq, IsTotallyUnimodular.one_fromCols, invOf_submatrix_equiv_eq, det_one_add_replicateCol_mul_replicateRow, zero_zpow_eq, Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec, mulVec_surjective_iff_exists_right_inverse, PEquiv.toMatrix_refl, isHermitian_one, mul_one, fromCols_one_isTotallyUnimodular_iff, TransvectionStruct.sumInl_toMatrix_prod_mul, Algebra.Norm.Transitivity.auxMat_toSquareBlock_ne, OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose, SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes, mem_orthogonalGroup_iff', LieAlgebra.Orthogonal.pso_inv, TransvectionStruct.reverse_inv_prod_mul_prod, LinearMap.toMatrix_basis_equiv, OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self, AffineBasis.toMatrix_self, den_one, one_apply_eq, isSymm_one, LieAlgebra.Orthogonal.indefiniteDiagonal_transform, LinearMap.toMatrix'_one, one_kroneckerTMul_one, LieAlgebra.Orthogonal.pb_inv, invOf_eq, TransvectionStruct.toMatrix_sumInl, vec_mul_eq_vecMul, IsTotallyUnimodular.fromRows_one, toLinearMapRight'_one, invertibleEquivDetInvertible_symm_apply, submatrixEquivInvertibleEquivInvertible_symm_apply, vec_mul_eq_mulVec, GeneralLinearGroup.coe_map_inv_mul_map, mul_nonsing_inv, zpow_neg_mul_zpow_self, permMatrix_refl, matPolyEquiv_smul_one, PEquiv.toMatrix_swap, Module.Basis.toMatrix_self, Algebra.Norm.Transitivity.auxMat_toSquareBlock_eq, ModularGroup.S_mul_S_eq, adjugate_mul, UnitaryGroup.star_mul_self, derivative_det_one_add_X_smul_aux, TensorProduct.toMatrix_comm, mul_adjp_add_detp, one_mulVec, invOf_fromBlocksββ_eq, one_mul, blockTriangular_one, transposeInvertibleEquivInvertible_apply, one_fin_two, transpose_list_prod, hadamard_one_eq_diagonal_iff, det_one_add_mul_comm, invOf_mul_cancel_left, det_invOf, blockDiagonal_one, LieAlgebra.Orthogonal.pd_inv, TransvectionStruct.mul_inv, one_div_zpow, conjTranspose_invOf, Fin.circulant_ite, mul_adjugate, comp_one, vecMul_one
|