| Name | Category | Theorems |
|---|
addMonoidHomMulLeft 📖 | CompOp | 1 mathmath: addMonoidHomMulLeft_apply
|
addMonoidHomMulRight 📖 | CompOp | 1 mathmath: addMonoidHomMulRight_apply
|
instHMulOfFintypeOfMulOfAddCommMonoid 📖 | CompOp | 492 mathmath: posSemidef_conjTranspose_mul_self, discr_conj, frobenius_nnnorm_mul, swap_mul_self, invOf_fromBlocks₂₂_eq, LinearMap.toMatrixAlgEquiv'_mul, isHermitian_conjTranspose_mul_mul, inv_mul_eq_iff_eq_mul_of_invertible, Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col, add_mul_mul_invOf_mul_eq_one, scalar_comm, posSemidef_iff_eq_conjTranspose_mul_self, toLinearMapRight'_mul, det_add_replicateCol_mul_replicateRow, PEquiv.single_mul_single_of_ne, replicateRow_mulVec, trace_mul_conjTranspose_self_eq_zero_iff, mul_mul_left, toLinearMap₂'_comp, SymplecticGroup.coe_inv, isHermitian_conjTranspose_mul_self, LinearMap.toMatrix₂_mul, lieConj_apply, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, mul_single_apply_same, LinearMap.toMatrixAlgEquiv_comp, IsHermitian.fromBlocks₂₂, Pivot.listTransvecCol_mul_last_col, LinearMap.BilinForm.toMatrix_compRight, mul_apply', mul_inv_eq_iff_eq_mul_of_invertible, posSemidef_self_mul_conjTranspose, mul_invOf_eq_iff_eq_mul_right, mul_smul, conjTranspose_mul_self_mulVec_eq_zero, inv_fromBlocks_zero₁₂_of_isUnit_iff, isHyperbolic_conj_iff, toLin_mul_apply, charpoly_units_conj', mul_right_injective_of_invertible, QuadraticMap.toMatrix'_comp, sum_hadamard_eq, mul_val_succ, exp_conj', toBlock_mul_eq_add, PosSemidef.commute_iff, Module.Basis.toMatrix_smul, map_mul_natCast, isHermitian_mul_conjTranspose_self, IsUnit.posSemidef_star_right_conjugate_iff, updateRow_mul, fromBlocks_eq_of_invertible₁₁, toLpLin_mul_same, isHyperbolic_conj'_iff, RingHom.map_matrix_mul, isElliptic_conj'_iff, rank_mul_le_right, PosDef.fromBlocks₁₁, addMonoidHomMulLeft_apply, sub_mul, charpoly_mul_comm_of_le, PosSemidef.conjTranspose_mul_mul_same, LinearMap.toMatrix₂'_compl₁₂, det_units_conj', mul_inv_of_invertible, AffineBasis.toMatrix_mul_toMatrix, toLin'_mul_apply, diag_replicateCol_mul_replicateRow, Algebra.Norm.Transitivity.comp_det_mul_pow, trace_mul_comm, Algebra.traceMatrix_of_matrix_vecMul, det_add_mul, LieAlgebra.Orthogonal.jb_transform, mul_right_inj_of_invertible, SymplecticGroup.mem_iff, ext_iff_trace_mul_right, Pivot.mul_listTransvecRow_last_col, mul_reindexLinearEquiv_one, ker_mulVecLin_conjTranspose_mul_self, SimpleGraph.mul_adjMatrix_apply, isParabolic_conj'_iff, mul_left_inj_of_invertible, toLinAlgEquiv_mul, mul_inv_cancel_right_of_invertible, inv_add_inv, transvection_mul_transvection_same, exp_add_of_commute, map_mul_ratCast, PosDef.conjTranspose_mul_mul_same, mem_unitaryGroup_iff, star_vec_dotProduct_vec, mul_assoc, mul_apply_eq_vecMul, LinearMap.BilinForm.mul_toMatrix'_mul, vec_dotProduct_vec, PEquiv.mul_toMatrix_apply, inv_sub_inv, BilinForm.mul_toMatrix_mul, zpow_add, zpow_add_of_nonneg, toLinearMap₂_compl₁₂, mulᵣ_eq, permMatrix_mul, Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec, LinearMap.toMatrix₂_compl₂, Commute.mul_zpow, eigenvalues_conjTranspose_mul_self_nonneg, adjugate_mul_distrib_aux, basis_toMatrix_basisFun_mul, submatrix_id_mul_right, fromBlocks_mul_fromRows, Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans, Fin.circulant_mul_comm, mul_updateCol, mulVec_vecMul, equiv_compl_fromCols_mul_fromRows_eq_one_comm, TransvectionStruct.inv_mul, LinearMap.toMatrix₂_comp, mul_neg, invOf_mul_eq_iff_eq_mul_left, addMonoidHomMulRight_apply, Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux, J_squared, nonsing_inv_mul, toBlock_mul_eq_mul, l2_opNorm_conjTranspose_mul_self, rank_mul_eq_right_of_isUnit_det, mul_kronecker_mul, toLin'_mul, isAdjointPair_equiv', mul_apply, PosSemidef.mul_mul_conjTranspose_same, LDL.lower_conj_diag, toLinearMapRight'_mul_apply, BilinForm.toMatrix_comp, isParabolic_conj_iff, toLin_mul, transvection_mul_apply_same, transpose_mul, mul_single_apply_of_ne, schur_complement_eq₂₂, op_smul_eq_mul_diagonal, single_mul_apply_same, TransvectionStruct.prod_mul_reverse_inv_prod, PEquiv.toMatrix_toPEquiv_mul, mul_zero, ext_iff_trace_mul_left, eigenvalues_self_mul_conjTranspose_nonneg, ker_mulVecLin_transpose_mul_self, vandermonde_transpose_mul_vandermonde, LinearMap.BilinForm.toMatrix'_compLeft, mul_mul_right, vecMulVec_mul, PosDef.conjTranspose_mul_self, mul_single_eq_updateCol_zero, Algebra.Norm.Transitivity.mul_auxMat_corner, vecMulVec_eq, reindexAlgEquiv_mul, trace_replicateCol_mul_replicateRow, TransvectionStruct.mul_sumInl_toMatrix_prod, det_one_sub_mul_comm, PosDef.commute_iff, add_mul_mul_invOf_mul_eq_one', mul_eq_one_comm_of_card_eq, LieAlgebra.SpecialLinear.sl_bracket, linearMap_toMatrix_mul_basis_toMatrix, Continuous.matrix_mul, rank_transpose_mul_self, fromRows_mul_fromCols, SimpleGraph.incMatrix_mul_transpose, isElliptic_conj_iff, isSymm_mul_transpose_self, det_fromBlocks₁₁, LinearMap.mul_toMatrix', l2_opNNNorm_mul, add_mul_mul_mul_invOf_eq_one, LinearMap.mul_toMatrix₂, det_fromBlocks_one₁₁, blockDiagonal'_mul, lieConj_symm_apply, kroneckerTMulLinearEquiv_mul, RootPairing.GeckConstruction.ω_mul_h, LinearMap.toMatrix'_mul, cons_mul, mul_basis_toMatrix, invOf_fromBlocks_zero₁₂_eq, single_mul_single_same, star_mul, one_submatrix_mul, diagonal_mul, smul_eq_mul_diagonal, posDef_iff_eq_conjTranspose_mul_self, vandermonde_mul_vandermonde_transpose, zpow_add_of_nonpos, replicateCol_mulVec, empty_mul_empty, IsHermitian.commute_iff, LinearMap.toMatrix_mul, LinearMap.toMatrix₂_compl₁₂, vecMul_conjTranspose_mul_self_eq_zero, CategoryTheory.HomOrthogonal.matrixDecomposition_comp, BilinForm.toMatrix_compRight, trace_conjTranspose_mul_self_eq_zero_iff, submatrix_id_mul_left, adjugate_mul_distrib, mul_fromCols, isUnit_fromBlocks_iff_of_invertible₂₂, det_conj', single_mul_mul_single, BlockTriangular.toBlock_inverse_mul_toBlock_eq_one, mul_invOf_cancel_right, swap_mul_apply_right, BilinForm.toMatrix_mul_basis_toMatrix, LinearMap.BilinForm.mul_toMatrix', mul_sub, charpoly_units_conj, fromBlocks_eq_of_invertible₂₂, UnitaryGroup.mul_val, isAdjointPair_equiv, rank_self_mul_conjTranspose, Nondegenerate.mul_iff_right, replicateRow_mul_replicateCol, trace_single_mul, schur_complement_eq₁₁, det_mul, invOf_add_mul_mul, Pivot.mul_listTransvecRow_last_row, add_mul, vec_vecMul_kronecker_of_commute, UnitaryGroup.mul_apply, sum_mul, mul_inv_cancel_left_of_invertible, det_fromBlocks_one₂₂, blockDiagonal_mul, zpow_add_one, SymplecticGroup.mem_iff', SymplecticGroup.inv_left_mul_aux, mul_add, isUnit_fromBlocks_iff_of_invertible₁₁, vecMul_surjective_iff_exists_left_inverse, diagonal_mul_diagonal', reindexLinearEquiv_mul, circulant_mul, exp_conj, PosDef.fromBlocks₂₂, mulRightLinearMap_apply, mul_adjp_apply_eq, RootPairing.GeckConstruction.ωConj_invFun, single_mul_single_of_ne, PEquiv.single_mul_single_right, mul_submatrix_one, scalar_comm_iff, Pivot.listTransvecCol_mul_last_row_drop, add_mul_mul_mul_invOf_eq_one', single_mul_eq_updateRow_zero, nonsing_inv_cancel_or_zero, LinearMap.toMatrix'_comp, toBilin'_comp, inv_mul_cancel_right_of_invertible, Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row, discr_conj', replicateRow_vecMul, mul_swap_of_ne, Module.Basis.toMatrix_mul_toMatrix_flip, LinearMap.mul_toMatrix₂_mul, mul_inv_rev, mul_right_eq_iff_eq_mul_invOf, mul_nonsing_inv_cancel_right, vecMul_vecMul, LinearMap.BilinForm.mul_toMatrix_mul, mul_swap_apply_left, circulant_mul_comm, RootPairing.GeckConstruction.ω_mul_ω, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix, exp_units_conj', LinearMap.BilinForm.toMatrix'_comp, Algebra.Norm.Transitivity.mul_auxMat_blockTriangular, mulLinearMap_apply_apply, pow_sub', RootPairing.GeckConstruction.ωConj_toFun, SimpleGraph.adjMatrix_mul_apply, LinearMap.BilinForm.toMatrix_mul, vec_vecMul_kronecker, mem_orthogonalGroup_iff, inv_mul_of_invertible, Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow, RootPairing.GeckConstruction.ω_mul_e, SimpleGraph.incMatrix_mul_transpose_diag, swap_mul_of_ne, mul_empty, dotProduct_vecMul_hadamard, self_mul_conjTranspose_mulVec_eq_zero, det_fromBlocks₂₂, LieAlgebra.Orthogonal.jd_transform, linfty_opNNNorm_mul, map_mul_intCast, mul_left_eq_iff_eq_invOf_mul, LinearMap.BilinForm.toMatrix_compLeft, det_conj, smul_mul, fromCols_mul_fromRows_eq_one_comm, Pivot.mul_listTransvecRow_last_col_take, Pivot.exists_isTwoBlockDiagonal_of_ne_zero, frobenius_norm_mul, LinearMap.BilinForm.mul_toMatrix, GeneralLinearGroup.coe_map_mul_map_inv, LinearMap.mul_toMatrix₂'_mul, LinearMap.toMatrix₂'_mul, det_mul_add_one_comm, kronecker_mulVec_vec, linfty_opNorm_mul, charpoly_mul_comm, PiLp.basis_toMatrix_basisFun_mul, BilinForm.toMatrix_mul, LinearMap.toMatrix_comp, kroneckerMapBilinear_mul_mul, detp_mul, LinearMap.toMatrix₂_mul_basis_toMatrix, Pivot.listTransvecCol_mul_last_row, mul_eq_one_comm_of_equiv, SimpleGraph.incMatrix_transpose_mul_diag, mul_transpose_self_isDiag_iff_hasOrthogonalRows, nonsing_inv_mul_cancel_right, trace_mul_single, mulRightLinearMap_mul, trace_transpose_mul, disc_conj, invOf_mul_cancel_right, inv_fromBlocks_zero₂₁_of_isUnit_iff, mul_invOf_cancel_left, Nondegenerate.mul_iff_left, mem_unitaryGroup_iff', toLpLin_mul, RootPairing.GeckConstruction.ω_mul_f, empty_mul, FixedDetMatrices.smul_def, mul_nonsing_inv_cancel_left, IsHermitian.fromBlocks₁₁, Algebra.traceMatrix_of_matrix_mulVec, two_mul_expl, Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal, invOf_add_mul_mul', Algebra.Norm.Transitivity.mul_auxMat_toSquareBlock_eq, mul_kroneckerTMul_mul, mul_right_injective_iff_mulVec_injective, PosDef.mul_mul_conjTranspose_same, vecMulVec_mul_vecMulVec, zero_mul, mul_left_injective_iff_vecMul_injective, mul_fin_two, LDL.diag_eq_lowerInv_conj, updateRow_zero_mul_updateCol_zero, self_mul_conjTranspose_mul_eq_zero, invOf_fromBlocks_zero₂₁_eq, BilinForm.mul_toMatrix, submatrix_mul_transpose_submatrix, rank_mul_le_left, toLpLin_symm_comp, det_one_add_replicateCol_mul_replicateRow, Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec, mulVec_surjective_iff_exists_right_inverse, det_mul_comm, nonsing_inv_mul_cancel_left, mul_adjp_apply_ne, LinearMap.BilinForm.toMatrix'_mul, zpow_sub_one, mul_one, LinearMap.toMatrix₂'_compl₂, fromRows_mul, diagonal_mul_diagonal, mul_transvection_apply_of_ne, det_mul_left_comm, TransvectionStruct.sumInl_toMatrix_prod_mul, neg_mul, charpoly_mul_comm', conjTranspose_mul_self_eq_zero, replicateRow_mul_replicateCol_apply, PEquiv.toMatrix_mul_apply, mul_fin_three, SimpleGraph.adjMatrix_mul_self_apply_self, FixedDetMatrices.smul_coe, mul_left_injective_of_invertible, IsUnit.posSemidef_star_left_conjugate_iff, GeneralLinearGroup.coe_mul, OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose, pow_inv_comm', basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, det_units_conj, mem_orthogonalGroup_iff', LieAlgebra.Orthogonal.pso_inv, rank_mul_eq_left_of_isUnit_det, transpose_mul_self_isDiag_iff_hasOrthogonalCols, Represents.mul, replicateCol_vecMul, submatrix_mul_equiv, disc_conj', fromBlocks_multiply, trace_mul_cycle, TransvectionStruct.reverse_inv_prod_mul_prod, OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self, vecMul_self_mul_conjTranspose_eq_zero, PosSemidef.sqrt_mul_self, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, mulLeftLinearMap_apply, isHermitian_mul_mul_conjTranspose, zpow_one_add, single_mul_apply_of_ne, BilinForm.toMatrix_compLeft, LinearMap.toMatrix₂'_comp, mulLeftLinearMap_mul, LinearMap.BilinForm.toMatrix_comp, l2_opNNNorm_conjTranspose_mul_self, swap_mul_apply_left, LieAlgebra.Orthogonal.indefiniteDiagonal_transform, isHermitian_transpose_mul_self, vec_mul_eq_vecMul, inner_matrix_row_row, toMvPolynomial_mul, map_mul, basis_toMatrix_mul_linearMap_toMatrix, skewAdjointMatricesLieSubalgebraEquiv_apply, conjTranspose_mul_self_mul_eq_zero, fromCols_mul_fromRows, vecMul_mulVec, PEquiv.mul_toMatrix_toPEquiv, rank_mul_le, vec_mul_eq_mulVec, GeneralLinearGroup.coe_map_inv_mul_map, mul_nonsing_inv, exp_units_conj, zpow_neg_mul_zpow_self, PEquiv.toMatrix_trans, LinearMap.toMatrixAlgEquiv_mul, trace_mul_cycle', det_mul_right_comm, l2_opNorm_mul, mul_diagonal, submatrix_mul, basis_toMatrix_mul, transvection_mul_apply_of_ne, smul_eq_diagonal_mul, ModularGroup.S_mul_S_eq, kronecker_mulVec_vec_of_commute, SpecialLinearGroup.coe_mul, adjugate_mul, Module.Basis.toMatrix_mul_toMatrix, UnitaryGroup.star_mul_self, self_mul_conjTranspose_eq_zero, conjTranspose_mul, inv_mul_cancel_left_of_invertible, mul_adjp_add_detp, mul_vecMulVec, isSymm_transpose_mul_self, zpow_add_one_of_ne_neg_one, mul_swap_apply_right, fromCols_mul_fromBlocks, Fin.circulant_mul, eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials, invOf_fromBlocks₁₁_eq, trace_conj', one_mul, IsUnit.posDef_star_left_conjugate_iff, RootPairing.GeckConstruction.lie_e_f_mul_ω, LinearMap.BilinForm.toMatrix'_compRight, PosDef.mul_conjTranspose_self, rank_conjTranspose_mul_self, SymplecticGroup.inv_eq_symplectic_inv, BlockTriangular.mul, Algebra.Norm.Transitivity.det_mul_corner_pow, LinearMap.toMatrixRight'_comp, det_one_add_mul_comm, mul_sum, trace_conj, invOf_mul_cancel_left, toBilin_comp, mul_transvection_apply_same, mulVecLin_mul, mul_self_mul_conjTranspose_eq_zero, det_comm, inner_matrix_col_col, LieAlgebra.Orthogonal.pd_inv, LinearMap.toMatrixAlgEquiv'_comp, mul_mul_apply, TransvectionStruct.mul_inv, PEquiv.single_mul_single, IsUnit.posDef_star_right_conjugate_iff, mul_adjugate, Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans, mulVec_mulVec, mul_conjTranspose_mul_self_eq_zero, SimpleGraph.incMatrix_mul_transpose_apply_of_adj, rank_self_mul_transpose
|
instMulOfFintypeOfAddCommMonoid 📖 | CompOp | 143 mathmath: l2_opNorm_toEuclideanCLM, list_prod_inv_reverse, invOf_fromBlocks₂₂_eq, transposeInvertibleEquivInvertible_symm_apply, kroneckerTMulStarAlgEquiv_symm_apply, Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col, add_mul_mul_invOf_mul_eq_one, Commute.zpow_self, cstar_nnnorm_def, SymplecticGroup.coe_inv, Pivot.listTransvecCol_mul_last_col, trace_units_conj, mul_invOf_eq_iff_eq_mul_right, RingCon.matrix_strictMono_of_nonempty, RingCon.matrix_top, mem_range_scalar_iff_commute_transvectionStruct, LinearMap.toMatrixOrthonormal_reindex, exists_right_inverse_iff_isUnit, PosSemidef.commute_iff, RingEquiv.mopMatrix_symm_apply, map_mul_natCast, fromBlocks_eq_of_invertible₁₁, RingEquiv.mopMatrix_apply, TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r, uniqueRingEquiv_apply, LinearMap.toMatrixOrthonormal_apply_apply, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, center_eq_range, Pivot.mul_listTransvecRow_last_col, map_mul_ratCast, transposeRingEquiv_symm_apply, piRingEquiv_apply, isSemisimpleRing_iff_pi_matrix_divisionRing, RingCon.ofMatrix_rel, toLinearEquiv'_symm_apply, piRingEquiv_symm_apply, Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec, TransvectionStruct.det_toMatrix_prod, toEuclideanCLM_toLp, invOf_eq_nonsing_inv, RingCon.coe_ofMatrix_eq_relationMap, isRegular_of_isLeftRegular_det, TransvectionStruct.toMatrix_reindexEquiv_prod, invOf_mul_eq_iff_eq_mul_left, Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux, mem_range_scalar_iff_commute_single, TransvectionStruct.prod_mul_reverse_inv_prod, LinearMap.toMatrixOrthonormal_symm_apply, instContinuousMulMatrixOfContinuousAdd, compRingEquiv_symm_apply, isRightRegular_iff_vecMul_injective, TransvectionStruct.mul_sumInl_toMatrix_prod, PosDef.commute_iff, add_mul_mul_invOf_mul_eq_one', ofLp_toEuclideanCLM, scalar_commute, kroneckerTMulStarAlgEquiv_apply, transposeRingEquiv_apply, det_fromBlocks₁₁, Commute.zpow_zpow_self, IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing, evalRingHom_mapMatrix_comp_compRingEquiv, RingEquiv.map_det, add_mul_mul_mul_invOf_eq_one, RingCon.ofMatrix_rel', invOf_fromBlocks_zero₁₂_eq, transpose_invOf, IsHermitian.commute_iff, mem_range_scalar_iff_commute_single', isUnit_fromBlocks_iff_of_invertible₂₂, mul_invOf_cancel_right, fromBlocks_eq_of_invertible₂₂, coe_toEuclideanCLM_eq_toEuclideanLin, conjTransposeRingEquiv_symm_apply, LinearMap.toMatrixOrthonormal_apply, invOf_add_mul_mul, Pivot.mul_listTransvecRow_last_row, RingEquiv.mapMatrix_apply, subsemigroupCenter_eq_scalar_map, isUnit_fromBlocks_iff_of_invertible₁₁, exists_left_inverse_iff_isUnit, Commute.self_zpow, IsSemisimpleModule.exists_end_ringEquiv, Pivot.listTransvecCol_mul_last_row_drop, add_mul_mul_mul_invOf_eq_one', RingCon.matrix_injective, RingCon.matrix_bot, Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row, uniqueRingEquiv_symm_apply, RingCon.matrix_apply_single, CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv, mul_right_eq_iff_eq_mul_invOf, invOf_diagonal_eq, Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing, det_fromBlocks₂₂, map_mul_intCast, mul_left_eq_iff_eq_invOf_mul, Pivot.mul_listTransvecRow_last_col_take, Pivot.exists_isTwoBlockDiagonal_of_ne_zero, submatrixEquivInvertibleEquivInvertible_apply, Pivot.listTransvecCol_mul_last_row, diagonalInvertibleEquivInvertible_symm_apply, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, invOf_mul_cancel_right, mul_invOf_cancel_left, diagonalInvertibleEquivInvertible_apply, invertibleEquivDetInvertible_apply, Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal, invOf_add_mul_mul', IsSimpleRing.exists_ringEquiv_matrix_divisionRing, commute_diagonal, conjTranspose_list_prod, invOf_fromBlocks_zero₂₁_eq, invOf_submatrix_equiv_eq, Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec, TransvectionStruct.sumInl_toMatrix_prod_mul, conjTransposeRingEquiv_apply, compRingEquiv_apply, TransvectionStruct.reverse_inv_prod_mul_prod, RingEquiv.mapMatrix_refl, trace_units_conj', cstar_norm_def, LieAlgebra.Orthogonal.pb_inv, invOf_eq, invertibleEquivDetInvertible_symm_apply, submatrixEquivInvertibleEquivInvertible_symm_apply, RingCon.matrix_apply, RingEquiv.mapMatrix_trans, scalar_commute_iff, kroneckerStarAlgEquiv_apply, invOf_fromBlocks₁₁_eq, RingCon.matrix_monotone, isLeftRegular_iff_mulVec_injective, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, transposeInvertibleEquivInvertible_apply, transpose_list_prod, center_eq_scalar_image, kroneckerStarAlgEquiv_symm_apply, invOf_mul_cancel_left, det_invOf, RingEquiv.mapMatrix_symm, conjTranspose_invOf
|
instMulOneOfFintypeOfDecidableEqOfAddCommMonoid 📖 | CompOp | 7 mathmath: permMatrixHom_apply, LinearMap.detAux_def, coe_detMonoidHom, instIsStablyFiniteRing, isStablyFiniteRing_iff, IsStablyFiniteRing.isDedekindFiniteMonoid, instIsDedekindFiniteMonoidOfIsStablyFiniteRing
|
instNonAssocRing 📖 | CompOp | — |
instNonUnitalRing 📖 | CompOp | 14 mathmath: IsHermitian.det_abs, PosSemidef.sqrt_eq_zero_iff, PosSemidef.det_sqrt, PosSemidef.posSemidef_sqrt, PosSemidef.sqrt_eq_one_iff, PosSemidef.sqrt_sq, PosSemidef.eq_sqrt_iff_sq_eq, instNonnegSpectrumClass, PosSemidef.isUnit_sqrt_iff, PosSemidef.sq_sqrt, PosSemidef.inv_sqrt, PosSemidef.sqrt_mul_self, PosDef.posDef_sqrt, PosSemidef.sqrt_eq_iff_eq_sq
|
instRing 📖 | CompOp | 134 mathmath: IsSymm.exp, IsHermitian.isClosedEmbedding_cfcAux, RootPairing.GeckConstruction.isSl2Triple, IsHermitian.det_abs, skewAdjointMatricesLieSubalgebraEquivTranspose_apply, RootPairing.GeckConstruction.instHasTrivialRadical, spectrum_toEuclideanLin, ModuleCat.toMatrixModCat_map, LieAlgebra.Orthogonal.mem_so, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, IsHermitian.cfc_eq, IsMoritaEquivalent.matrix, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, lieConj_apply, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, isSkewAdjoint_bracket, spectrum_toLpLin, ModuleCat.matrixEquivalence_inverse, LieModule.instIsFaithfulMatrixForall, TwoSidedIdeal.matrix_jacobson_bot, ModuleCat.toMatrixModCat_obj_carrier, PosSemidef.sqrt_eq_zero_iff, mem_spectrum_iff_isRoot_charpoly, exp_conj', exp_neg, ModuleCat.toMatrixModCat_obj_isAddCommGroup, LinearMap.spectrum_toMatrix', spectrum_diagonal, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, minpoly_dvd_charpoly, LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, Subring.coe_matrix, exp_add_of_commute, PosSemidef.det_sqrt, TwoSidedIdeal.jacobson_matrix, mem_spectrum_of_isRoot_charpoly, IsHermitian.charpoly_cfc_eq, ModuleCat.matrixEquivalence_functor, PosSemidef.posSemidef_sqrt, IsHermitian.exp, finite_spectrum, Ideal.single_mem_jacobson_matrix, PosSemidef.sqrt_eq_one_iff, PosSemidef.sqrt_sq, lieEquivMatrix'_apply, LinearMap.minpoly_toMatrix', PosSemidef.eq_sqrt_iff_sq_eq, exp_diagonal, instFiniteSpectrum, RootPairing.GeckConstruction.trace_toEnd_eq_zero, instLieModuleForall, exp_nsmul, exp_zsmul, RootPairing.GeckConstruction.span_range_h'_eq_top, MatrixModCat.toModuleCat_obj_carrier, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', reindexLieEquiv_apply, IsHermitian.cfcAux_apply, LieAlgebra.SpecialLinear.sl_bracket, exp_conjTranspose, reindexLieEquiv_symm, instFiniteElemRealSpectrum, exp_transpose, mem_skewAdjointMatricesLieSubalgebra, lieConj_symm_apply, matPolyEquiv_charmatrix, RootPairing.GeckConstruction.instIsIrreducible, LinearMap.spectrum_toMatrix, ModuleCat.matrixEquivalence_unitIso, minpoly_toLin', RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, lie_apply, PosSemidef.isUnit_sqrt_iff, LinearMap.minpoly_toMatrix, IsHermitian.spectrum_eq_image_range, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, Ideal.matrix_jacobson_le, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, exp_conj, PosSemidef.sq_sqrt, RootPairing.GeckConstruction.ωConj_invFun, spectrum_toLin, IsSemisimpleRing.instMatrix, PosSemidef.inv_sqrt, finite_real_spectrum, exp_blockDiagonal, mem_skewAdjointMatricesLieSubalgebra_unit_smul, ModuleCat.matrixEquivalence_counitIso, RootPairing.GeckConstruction.f_lie_v_ne, exp_units_conj', LieAlgebra.matrix_trace_commutator_zero, RootPairing.GeckConstruction.ωConj_toFun, MatrixModCat.isScalarTower_toModuleCat, RootPairing.GeckConstruction.e_lie_v_ne, LieAlgebra.SpecialLinear.val_single, lieEquivMatrix'_symm_apply, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, RootPairing.GeckConstruction.h_mem_lieAlgebra, IsHermitian.spectrum_real_eq_range_eigenvalues, lie_transpose, IsHermitian.cfcAux_id, MatrixModCat.toModuleCat_map, RootPairing.GeckConstruction.lie_e_lie_f_apply, IsHermitian.eigenvalues_mem_spectrum_real, isUnit_exp, RootPairing.GeckConstruction.f_lie_v_same, MatrixModCat.toModuleCat_obj_isAddCommGroup, TwoSidedIdeal.asIdeal_matrix, PosSemidef.sqrt_mul_self, RootPairing.GeckConstruction.f_mem_lieAlgebra, exp_blockDiagonal', RootPairing.GeckConstruction.e_mem_lieAlgebra, LieAlgebra.SpecialLinear.val_singleSubSingle, skewAdjointMatricesLieSubalgebraEquiv_apply, exp_units_conj, minpoly_toLin, isIntegral, matPolyEquiv_eq_X_pow_sub_C, subringCenter_eq_scalar_map, MatrixModCat.toModuleCat_obj_isModule, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, PosDef.posDef_sqrt, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', IsHermitian.instContinuousFunctionalCalculus, posSemidef_iff_isHermitian_and_spectrum_nonneg, RootPairing.GeckConstruction.e_lie_u, PosSemidef.sqrt_eq_iff_eq_sq, LieModule.toEnd_matrix, LieAlgebra.SpecialLinear.sl_non_abelian, spectrum_toLin', moritaEquivalenceMatrix_eqv, ModuleCat.toMatrixModCat_obj_isModule
|
mulVec 📖 | CompOp | 175 mathmath: mulVec_transpose, empty_mulVec, det_smul_inv_mulVec_eq_cramer, Nat.isLinearSet_iff_exists_matrix, SimpleGraph.adjMatrix_mulVec_apply, replicateRow_mulVec, l2_opNorm_mulVec, zero_mulVec, repr_toLin, add_mulVec, SimpleGraph.dotProduct_mulVec_adjMatrix, conjTranspose_mul_self_mulVec_eq_zero, mulVec_injective, PEquiv.toMatrix_toPEquiv_mulVec, mulVec_single_one, swap_mulVec_apply, coe_mulVecLin, mulVecLin_apply, posDef_iff_dotProduct_mulVec, IsHermitian.eigenvalues_eq, star_dotProduct_toMatrix₂_mulVec, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, IsCoprime.mulVecSL, neg_mulVec_neg, toEuclideanLin_apply, mulVecᵣ_eq, linfty_opNNNorm_mulVec, LDL.lowerInv_orthogonal, toLinearMap₂'_apply', LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec, IsHermitian.eigenvectorUnitary_mulVec, mulVec_one_of_mem_doublyStochastic, SimpleGraph.dotProduct_mulVec_degMatrix, SimpleGraph.lapMatrix_mulVec_const_eq_zero, star_vecMul, toEuclideanCLM_toLp, nonneg_mulVec_of_mem_colStochastic, BilinForm.dotProduct_toMatrix_mulVec, replicateRow_mulVec_eq_const, mul_updateCol, mulVec_vecMul, toPerfectPairing_apply_apply, l2_opNNNorm_mulVec, LinearMap.BilinForm.dotProduct_toMatrix_mulVec, submatrix_mulVec_equiv, mulVec_sum, NumberField.house.exists_ne_zero_int_vec_house_le, GeneralLinearGroup.toLin'_apply, mulVec_surjective_of_invertible, schur_complement_eq₂₂, ext_iff_mulVec, LinearMap.toMatrix_mulVec_repr, toLin_apply_eq_zero_iff, fromBlocks_mulVec, PosSemidef.toLinearMap₂'_zero_iff, apply_eq_dotProduct_toMatrix₂_mulVec, Algebra.discr_of_matrix_mulVec, ofLp_toEuclideanCLM, neg_mulVec, Continuous.matrix_mulVec, mulVec_zero, SimpleGraph.adjMatrix_mulVec_const_apply, replicateCol_mulVec, toLinAlgEquiv'_apply, apply_eq_star_dotProduct_toMatrix₂_mulVec, exists_mulVec_eq_zero_iff, Nat.isSemilinearSet_setOf_mulVec_eq, mulVec_smul, represents_iff, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, lie_apply, Represents.congr_fun, SimpleGraph.lapMatrix_mulVec_apply, schur_complement_eq₁₁, toMvPolynomial_eval_eq_apply, toLin_apply, RingHom.map_mulVec, mulVec_injective_of_isUnit, circulant_mul, diagonal_mulVec_single, mulVec_eq_sum, NumberField.inverse_basisMatrix_mulVec_eq_repr, ofNat_mulVec, linfty_opNorm_mulVec, mulVec_add, PosSemidef.dotProduct_mulVec_nonneg, toLpLinAlgEquiv_apply_apply_ofLp, mulVec_conjTranspose, toLinAlgEquiv_apply, IsHermitian.exists_eigenvector_of_ne_zero, ofLp_toEuclideanLin_apply, swap_mulVec, vecMul_conjTranspose, mulVecBilin_apply, permMatrix_mulVec, self_mul_conjTranspose_mulVec_eq_zero, toBilin'_apply', smul_eq_mulVec, star_dotProduct_gram_mulVec, kronecker_mulVec_vec, PosSemidef.re_dotProduct_nonneg, nonneg_mulVec_of_mem_rowStochastic, mulVec_neg, posSemidef_iff_dotProduct_mulVec, mulVec_cramer, sub_mulVec, PosSemidef.dotProduct_mulVec_zero_iff, mem_doublyStochastic, natCast_mulVec, PiToModule.fromMatrix_apply, toEuclideanLin_apply_piLp_toLp, Algebra.traceMatrix_of_matrix_mulVec, Algebra.leftMulMatrix_mulVec_repr, SimpleGraph.adjMatrix_mulVec_const_apply_of_regular, diagonal_const_mulVec, mul_right_injective_iff_mulVec_injective, isNilpotent_iff, mulVec_surjective_iff_exists_right_inverse, SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_reachable, mulVec_surjective_iff_isUnit, mulVec_empty, sum_mulVec, Algebra.traceMatrix_of_basis_mulVec, vecMulVec_mulVec, cons_mulVec, single_mulVec, mulVec_injective_iff, SimpleGraph.degMatrix_mulVec_apply, updateRow_mulVec, fromCols_mulVec_sumElim, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, mulVec_single, mem_rowStochastic, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, mulVec_diagonal, intCast_mulVec, vecMul_transpose, vecMul_mulVec, fromRows_mulVec, toLpLin_apply, vec_mul_eq_mulVec, toLin'_apply, IsHermitian.mulVec_eigenvectorBasis, mulVec_cons, mulVec_sub, kronecker_mulVec_vec_of_commute, mulVec.addMonoidHomLeft_apply, fromCols_mulVec, Module.Basis.toMatrix_mulVec_repr, mulVec_dotProduct_one_eq_one_colStochastic, mul_vecMulVec, mulVec_one, mulVec_injective_of_invertible, Fin.circulant_mul, one_mulVec, LinearMap.toMatrix'_mulVec, dotProduct_toMatrix₂_mulVec, sum_mulVec_of_mem_doublyStochastic, isLeftRegular_iff_mulVec_injective, smul_mulVec, IsHermitian.star_eigenvectorUnitary_mulVec, Int.Matrix.exists_ne_zero_int_vec_norm_le, mulVec_injective_iff_isUnit, SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_adj, sum_mulVec_of_mem_colStochastic, IsHermitian.im_star_dotProduct_mulVec_self, PosDef.dotProduct_mulVec_pos, mul_mul_apply, cramer_eq_adjugate_mulVec, dotProduct_mulVec, PosDef.re_dotProduct_pos, Int.Matrix.exists_ne_zero_int_vec_norm_le', mulVec_mulVec, star_mulVec, one_vecMul_of_mem_rowStochastic
|
nonAssocSemiring 📖 | CompOp | 131 mathmath: UnitaryGroup.toLin'_one, RingHom.mapMatrix_id, SymplecticGroup.transpose_mem_iff, scalar_inj, reindex_mem_doublyStochastic_iff, Algebra.Norm.Transitivity.polyToMatrix_cornerAddX, scalar_comm, UnitaryGroup.toGL_mul, det_det, SymplecticGroup.coe_inv, isParabolic_iff_exists, SymplecticGroup.coe_J, reindex_mem_colStochastic_iff, GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, specialUnitaryGroup_le_unitaryGroup, RingHom.mapMatrix_apply, mem_doublyStochastic_iff_sum, SpecialLinearGroup.scalar_eq_self_of_mem_center, blockDiagonal'RingHom_apply, permMatrix_mem_rowStochastic, mem_range_scalar_iff_commute_transvectionStruct, Algebra.map_leftMulMatrix_localization, Algebra.traceMatrix_localizationLocalization, IsHermitian.eigenvectorUnitary_col_eq, Algebra.Norm.Transitivity.comp_det_mul_pow, center_eq_range, SymplecticGroup.mem_iff, IsHermitian.eigenvectorUnitary_mulVec, IsParabolic.sub_eigenvalue_sq_eq_zero, mem_unitaryGroup_iff, charpoly_sub_scalar, SpecialLinearGroup.map_apply_coe, mem_specialOrthogonalGroup_iff, reindex_mem_rowStochastic_iff, doublyStochastic_eq_rowStochastic_inf_colStochastic, toLin_scalar, subsemiringCenter_eq_scalar_map, UnitaryGroup.one_apply, LinearMap.mapMatrixModule_apply, GeneralLinearGroup.fixpointPolynomial_eq_zero_iff, LinearMap.mapMatrixModule_id_apply, LinearMap.toMatrix'_algebraMap, mem_range_scalar_iff_commute_single, UnitaryGroup.one_val, evalRingHom_mapMatrix_comp_polyToMatrix, convex_colStochastic, projVandermonde_map, UnitaryGroup.det_isUnit, SpecialLinearGroup.scalar_eq_coe_self_center, scalar_commute, evalRingHom_mapMatrix_comp_compRingEquiv, UnitaryGroup.inv_val, scalarAlgHom_apply, LinearMap.toMatrix_algebraMap, Module.scalar_smul, submonoidCenter_eq_scalar_map, mem_range_scalar_iff_commute_single', transpose_mem_rowStochastic_iff_mem_colStochastic, mem_specialUnitaryGroup_iff, Polynomial.sylvester_map_map, UnitaryGroup.mul_val, sub_scalar_sq_eq_disc, IsHermitian.eigenvectorUnitary_apply, mem_rowStochastic_iff_sum, Algebra.Norm.Transitivity.eval_zero_comp_det, UnitaryGroup.mul_apply, mem_doublyStochastic_iff_mem_rowStochastic_and_mem_colStochastic, subsemigroupCenter_eq_scalar_map, SymplecticGroup.mem_iff', UnitaryGroup.ext_iff, doublyStochastic_eq_convexHull_permMatrix, eval_det, RingHom.map_adjugate, GeneralLinearGroup.mem_center_iff_val_eq_scalar, mem_range_scalar_of_commute_single, scalar_comm_iff, mvPolynomialX_mapMatrix_eval, IsHermitian.eigenvectorUnitary_coe, RingHom.map_det, star_eq_inv, diagonalRingHom_apply, mem_orthogonalGroup_iff, eval_charpoly, extremePoints_doublyStochastic, SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, matPolyEquiv_eval_eq_map, of_mem_specialOrthogonalGroup_fin_two_iff, mem_colStochastic, mem_colStochastic_iff_sum, specialUnitaryGroup.coe_star, OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary, mem_doublyStochastic, circulant_single, mem_unitaryGroup_iff', convex_rowStochastic, Subsemiring.coe_matrix, permMatrix_mem_colStochastic, matPolyEquiv_symm_map_eval, mem_specialOrthogonalGroup_fin_two_iff, Algebra.Norm.Transitivity.eval_zero_det_det, convex_doublyStochastic, matPolyEquiv_eval, RingHom.mapMatrix_comp, SymplecticGroup.coe_inv', IsHermitian.eigenvectorUnitary_transpose_apply, UnitaryGroup.toLin'_mul, mem_orthogonalGroup_iff', blockDiagonalRingHom_apply, transpose_mem_doublyStochastic_iff, UnitaryGroup.toGL_one, OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal, scalar_apply, mem_rowStochastic, mem_range_scalar_of_commute_transvectionStruct, transpose_mem_colStochastic_iff_mem_rowStochastic, permMatrix_mem_doublyStochastic, Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, scalar_commute_iff, matPolyEquiv_eq_X_pow_sub_C, UnitaryGroup.star_mul_self, sub_scalar_sq_eq_discr, IsHermitian.star_eigenvectorUnitary_mulVec, SymplecticGroup.J_mem, Module.Basis.restrictScalars_toMatrix, center_eq_scalar_image, exists_mem_doublyStochastic_eq_smul_iff, algebraMap_eq_diagonalRingHom, LinearMap.mapMatrixModule_comp_apply, SpecialLinearGroup.mem_center_iff, UnitaryGroup.inv_apply, charmatrix_zero
|
nonUnitalNonAssocRing 📖 | CompOp | 32 mathmath: Subgroup.adjoinNegOne_eq_self_iff, Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular, TwoSidedIdeal.equivMatrix_symm_apply_ringCon, TwoSidedIdeal.matrix_jacobson_bot, UpperHalfPlane.num_neg, TwoSidedIdeal.equivMatrix_apply, TwoSidedIdeal.matrix_top, TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r, Subgroup.mem_adjoinNegOne_iff, TwoSidedIdeal.matrix_bot, RootPairing.GeckConstruction.lie_h_e, TwoSidedIdeal.mem_matrix, Subgroup.negOne_mem_adjoinNegOne, GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_det, UpperHalfPlane.σ_neg, IsSimpleRing.matrix, TwoSidedIdeal.coe_equivMatrix_symm_apply, UpperHalfPlane.denom_neg, exp_blockDiagonal, RootPairing.GeckConstruction.lie_e_f_same, TwoSidedIdeal.orderIsoMatrix_symm_apply_ringCon_r, RootPairing.GeckConstruction.lie_h_f, topologicalRing, TwoSidedIdeal.matrix_monotone, exp_blockDiagonal', TwoSidedIdeal.matrix_ringCon, RootPairing.GeckConstruction.lie_h_h, UpperHalfPlane.neg_smul, GLPos.coe_neg_GL, RootPairing.GeckConstruction.lie_e_f_mul_ω, TwoSidedIdeal.matrix_strictMono_of_nonempty, RootPairing.GeckConstruction.lie_e_f_ne
|
nonUnitalNonAssocSemiring 📖 | CompOp | 12 mathmath: kroneckerTMulStarAlgEquiv_symm_apply, Semiring.smulCommClass, mulRightLinearMap_eq_mulRight, kroneckerTMulStarAlgEquiv_apply, kroneckerTMulLinearEquiv_mul, MatrixEquivTensor.invFun_smul, mulLeftLinearMap_eq_mulLeft, instIsTopologicalSemiringMatrix, Semiring.isScalarTower, kroneckerStarAlgEquiv_apply, mulLinearMap_eq_mul, kroneckerStarAlgEquiv_symm_apply
|
nonUnitalSemiring 📖 | CompOp | 1 mathmath: instStarOrderedRing
|
semiring 📖 | CompOp | 516 mathmath: LinearMap.restrictScalars_toMatrix, discr_conj, toLinAlgEquiv_one, GeneralLinearGroup.det_scalar, ModularGroup.SLOnGLPos_smul_apply, Algebra.IsCentral.matrix, ModularForm.smul_slash, LinearMap.toMatrixAlgEquiv'_mul, GLPos.coe_neg_apply, kroneckerTMulStarAlgEquiv_symm_apply, Subgroup.adjoinNegOne_eq_self_iff, IsHermitian.isClosedEmbedding_cfcAux, SpecialLinearGroup.map_mapGL, isUnit_of_right_inverse, GeneralLinearGroup.map_det, GeneralLinearGroup.val_mkOfDetNeZero, SpecialLinearGroup.continuous_toGL, pow_eq_aeval_mod_charpoly, Subgroup.instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL, IsHermitian.det_abs, ModularForm.mul_slash, one_div_pow, GeneralLinearGroup.IsParabolic.parabolicFixedPoint_pow, SpecialLinearGroup.coeToGL_det, compAlgEquiv_apply, GeneralLinearGroup.map_comp_apply, UpperHalfPlane.re_smul, Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL, SpecialLinearGroup.toGLPos_injective, LinearMap.toMatrixAlgEquiv_comp, isParabolic_iff_exists, Algebra.norm_eq_matrix_det, ZMod.charpoly_pow_card, GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, CongruenceSubgroup.exists_Gamma_le_conj', trace_units_conj, isNilpotent_transpose_iff, SlashInvariantForm.quotientFunc_mk, ModularForm.SL_slash, CongruenceSubgroup.conjGL_coe, UpperHalfPlane.im_smul_eq_div_normSq, isHyperbolic_conj_iff, GeneralLinearGroup.map_inv_mul_map, charpoly_units_conj', PosSemidef.sqrt_eq_zero_iff, UpperHalfPlane.num_neg, UpperHalfPlane.moebius_im, ModularForm.prod_slash, Algebra.smul_leftMulMatrix, LinearMap.toMatrixAlgEquiv_toLinAlgEquiv, OnePoint.smul_infty_eq_self_iff, GeneralLinearGroup.coe_toLin, CongruenceSubgroup.strictPeriods_Gamma0, Algebra.map_leftMulMatrix_localization, exists_right_inverse_iff_isUnit, matPolyEquiv_map_smul, Module.Basis.toMatrix_smul, ModularForm.norm_eq_zero_iff, diagonal_pow, matPolyEquiv_diagonal_X, toMatrix_rotation, GeneralLinearGroup.isParabolic_conj_iff, ZMod.trace_pow_card, AlgHom.mulLeftRightMatrix.inv_comp, ModularForm.prod_slash_sum_weights, IsSymm.pow, isHyperbolic_conj'_iff, ModularGroup.coe_apply_complex, ModularForm.levelOne_neg_weight_rank_zero, Subgroup.IsArithmetic.is_commensurable, Subgroup.IsArithmetic.inter, isElliptic_conj'_iff, ModularGroup.sl_moeb, GeneralLinearGroup.center_eq_range_scalar, isNilpotent_iff_forall_row, Algebra.toMatrix_lmul_eq, Subgroup.instHasDetOneMinGeneralLinearGroup_1, LinearMap.toMatrixAlgEquiv'_id, CuspForm.coe_trace, instSMulCommClassMatrixFinOfNatNatProd, UpperHalfPlane.J_sq, CongruenceSubgroup.exists_Gamma_le_conj, det_units_conj', PosSemidef.sq_eq_sq_iff, coe_units_inv, UpperHalfPlane.denom_cocycle_σ, Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL, SpecialLinearGroup.isClosedEmbedding_toGL, LinearMap.toMatrixAlgEquiv_apply, Subgroup.mem_adjoinNegOne_iff, toAlgEquiv_kroneckerStarAlgEquiv, PosSemidef.posDef_iff_isUnit, isParabolic_conj'_iff, Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex, toLinAlgEquiv_mul, SlashInvariantForm.coe_translate, instSMulCommClassForall_1, GeneralLinearGroup.upperRightHom_apply, PosSemidef.det_sqrt, Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, GeneralLinearGroup.val_mk'', toAlgEquiv_kroneckerTMulStarAlgEquiv, matPolyEquiv_coeff_apply_aux_1, isCusp_SL2Z_iff', IsParabolic.sub_eigenvalue_sq_eq_zero, ModularGroup.lcRow0Extend_symm_apply, Algebra.leftMulMatrix_injective, ModularGroup.denom_apply, isNilpotent_toLin'_iff, LinearMap.detAux_def, matPolyEquiv_symm_apply_coeff, OnePoint.smul_some_eq_ite, GeneralLinearGroup.continuous_det, LinearMap.toMatrixAlgEquiv_id, isUnits_det_units, UpperHalfPlane.σ_mul, PowerBasis.leftMulMatrix, PosSemidef.posSemidef_sqrt, Subgroup.commensurable_adjoinNegOne_self, toLpLin_symm_pow, PosDef.isUnit, isUnit_fromBlocks_zero₂₁, AlgEquiv.mopMatrix_apply, pow_apply_nonneg, isRepresentation.toEnd_represents, Subgroup.strictWidthInfty_eq_one_of_T_mem, det_reindexAlgEquiv, PosSemidef.sqrt_eq_one_iff, PosSemidef.sqrt_sq, charpoly_leftMulMatrix, Subgroup.negOne_mem_adjoinNegOne, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, SpecialLinearGroup.mapGL_injective, ModularGroup.SL_to_GL_tower, ModularFormClass.one_mem_strictPeriods_SL2Z, OnePoint.map_smul, SpecialLinearGroup.mapGL_inj, GeneralLinearGroup.IsParabolic.pow, PosSemidef.eq_sqrt_iff_sq_eq, AlgHom.map_adjugate, TransvectionStruct.toMatrix_reindexEquiv_prod, AlgEquiv.mapMatrix_refl, ModularForm.levelOne_weight_zero_rank_one, CongruenceSubgroup.strictWidthInfty_Gamma0, pow_apply_pos_iff_nonempty_path, toLpLin_pow, CongruenceSubgroup.IsArithmetic.conj, kroneckerAlgEquiv_apply, map_algebraMap, isUnit_toLin'_iff, UpperHalfPlane.denom_cocycle, GeneralLinearGroup.coe_one, ModularGroup.lcRow0Extend_apply, LinearMap.isNilpotent_toMatrix_iff, isUnit_submatrix_equiv, Module.smul_def, GeneralLinearGroup.val_mk', GeneralLinearGroup.map_comp, exp_nsmul, TransvectionStruct.toMatrix_reindexEquiv, LinearMap.mapMatrixModule_apply, SpecialLinearGroup.isClosedEmbedding_mapGLInt, Subgroup.IsArithmetic.isFiniteRelIndexSL, AlgHom.map_det, GeneralLinearGroup.map_inv, isParabolic_conj_iff, toLin_pow, Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem, GeneralLinearGroup.fixpointPolynomial_eq_zero_iff, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, GeneralLinearGroup.toLin'_apply, LinearMap.mapMatrixModule_id_apply, LinearMap.toMatrixAlgEquiv'_apply, CongruenceSubgroup.isArithmetic_conj_SL2Z, fin_two_smul_prod, EisensteinSeries.q_expansion_riemannZeta, AlgHom.mapMatrix_apply, ModularGroup.denom_S, SimpleGraph.IsSRGWith.matrix_eq, exp_sum_of_commute, uniqueAlgEquiv_apply, SpecialLinearGroup.isInducing_mapGL, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing, GeneralLinearGroup.continuous_upperRightHom, UpperHalfPlane.im_smul, OnePoint.IsZeroAt.smul_iff, SimpleGraph.adjMatrix_pow_apply_eq_card_walk, UpperHalfPlane.σ_neg, instIsFiniteRelIndexGeneralLinearGroupAdjoinNegOne, UpperHalfPlane.coe_smul, isRepresentation.toEnd_exists_mem_ideal, reindexAlgEquiv_mul, AlgHom.mapMatrix_comp, pow_mulLeftLinearMap, isStrictlyPositive_iff_posDef, Ideal.mem_matrix, IsHermitian.cfcAux_apply, kroneckerTMulAlgEquiv_symm_apply, GeneralLinearGroup.ext_iff, kroneckerTMulStarAlgEquiv_apply, AlgEquiv.mapMatrix_symm, MDifferentiable.slash, isElliptic_conj_iff, GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, nonsing_inv_eq_ringInverse, CuspForm.coe_translate, pow_mulRightLinearMap, UnitaryGroup.inv_val, MatrixModCat.mem_toModuleCatObj, scalarAlgHom_apply, val_planeConformalMatrix, kroneckerTMulLinearEquiv_mul, Ideal.matrix_top, IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite, linearIndependent_cols_iff_isUnit, dualNumberEquiv_symm_apply, Subgroup.isArithmetic_iff_finiteIndex, matPolyEquiv_charmatrix, isIrreducible_iff_exists_pow_pos, SpecialLinearGroup.toGL_injective, Module.instIsScalarTowerForall, isUnit_toLin_iff, posDef_iff_eq_conjTranspose_mul_self, Module.scalar_smul, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, toLin'_pow, Subalgebra.coe_matrix, instSMulCommClassMulOppositeForallOfIsScalarTower_1, Subgroup.instHasDetOneMinGeneralLinearGroup, instIsNoetherianRingMatrix, toLinAlgEquiv'_apply, isCusp_SL2Z_iff, Algebra.smulTower_leftMulMatrix, surjective_cosetToCuspOrbit, CongruenceSubgroup.strictWidthInfty_Gamma1, isUnit_fromBlocks_iff_of_invertible₂₂, UpperHalfPlane.J_smul, LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv', EisensteinSeries.eisensteinSeries_SIF_apply, algebraMap_eq_diagonal, PosSemidef.isUnit_sqrt_iff, reindexAlgEquiv_symm, IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed, UpperHalfPlane.denom_neg, charpoly_units_conj, FiniteField.Matrix.charpoly_pow_card, GeneralLinearGroup.isParabolic_conj_iff', CongruenceSubgroup.finiteIndex_conjGL, sub_scalar_sq_eq_disc, LinearMap.toMatrixAlgEquiv_symm, isUnit_iff_isUnit_det, FiniteField.trace_pow_card, IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite, matrixEquivTensor_apply_single, SpecialLinearGroup.range_toGL, matPolyEquiv_map_C, SpecialLinearGroup.isEmbedding_toGL, Algebra.leftMulMatrix_complex, SpecialLinearGroup.coe_GLPos_neg, MatrixEquivTensor.invFun_smul, isUnit_fromBlocks_zero₁₂, SpecialLinearGroup.coe_pow, matrixEquivTensor_apply_symm, isUnit_fromBlocks_iff_of_invertible₁₁, Ideal.matrix_jacobson_le, exists_left_inverse_iff_isUnit, ModularForm.SL_slash_def, Module.smul_apply, OnePoint.smul_infty_eq_ite, MatrixEquivTensor.left_inv, Algebra.smulTower_leftMulMatrix_algebraMap_ne, eval_det, IsHermitian.spectral_theorem, diagonalAlgHom_apply, PosSemidef.sq_sqrt, GeneralLinearGroup.mem_center_iff_val_eq_scalar, UpperHalfPlane.coe_J_smul, endVecAlgEquivMatrixEnd_apply_apply, GeneralLinearGroup.map_swap, CongruenceSubgroup.strictPeriods_Gamma1, PosDef.isStrictlyPositive, OnePoint.IsBoundedAt.smul_iff, AlgHom.mapMatrix_id, Algebra.trace_eq_matrix_trace, inv_pow', matPolyEquiv_symm_C, LinearMap.mapMatrixModule_comp, LinearMap.isUnit_toMatrix'_iff, GeneralLinearGroup.coe_inv, SlashInvariantForm.coe_trace, PosSemidef.inv_sqrt, compAlgEquiv_symm_apply, discr_conj', PosSemidef.pow, isUnit_comp_iff, isUnit_conjTranspose, SlashInvariantForm.slash_action_eqn_SL'', CongruenceSubgroup.strictWidthInfty_Gamma, IsSemisimpleModule.exists_end_algEquiv, RootPairing.GeckConstruction.isNilpotent_f, toLpLinAlgEquiv_apply_apply_ofLp, toLinAlgEquiv_apply, exp_units_conj', IsPrimitive.exists_pos_pow, EisensteinSeries.q_expansion_bernoulli, pow_sub', Algebra.smulTower_leftMulMatrix_algebraMap, MatrixModCat.isScalarTower_toModuleCat, instIsScalarTowerForall, GeneralLinearGroup.map_mul_map_inv, transpose_pow, GeneralLinearGroup.val_inv_det_apply, reindexAlgEquiv_refl, Module.single_smul, RootPairing.GeckConstruction.isNilpotent_e, GeneralLinearGroup.center_eq_range_units, ModularGroup.im_smul_eq_div_normSq, SpecialLinearGroup.coe_GL_coe_matrix, LinearMap.isUnit_toMatrix_iff, matPolyEquiv_eval_eq_map, smul_eq_mulVec, CongruenceSubgroup.mem_conjGL, matPolyEquiv_coeff_apply, piAlgEquiv_symm_apply, vecMul_injective_iff_isUnit, GeneralLinearGroup.coe_map_mul_map_inv, SpecialLinearGroup.coe_to_GLPos_to_GL_det, OnePoint.smul_infty_def, conjTranspose_pow, isRepresentation.toEnd_surjective, CongruenceSubgroup.strictPeriods_Gamma, cosetToCuspOrbit_apply_mk, toLinAlgEquiv_self, kroneckerAlgEquiv_symm_apply, GeneralLinearGroup.val_inv_scalar_apply, isUnit_nonsing_inv_iff, OnePoint.exists_mem_SL2, instSMulCommClassForall, IsHermitian.cfcAux_id, mem_glpos, Subgroup.le_adjoinNegOne, blockDiagonal_pow, AlgEquiv.map_det, disc_conj, LinearMap.toMatrixAlgEquiv'_symm, GeneralLinearGroup.val_map_apply, LinearMap.mapMatrixModule_id, uniqueAlgEquiv_symm_apply, transposeAlgEquiv_apply, AffineBasis.isUnit_toMatrix_iff, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, UpperHalfPlane.det_J, ModularGroup.coe_one, IsHermitian.pow, ModularForm.coe_norm, Subgroup.strictPeriods_SL2Z, CongruenceSubgroup.mem_conjGL', subalgebraCenter_eq_scalarAlgHom_map, reindexAlgEquiv_apply, Algebra.leftMulMatrix_mulVec_repr, ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, Subgroup.mem_strictPeriods_iff, dualNumberEquiv_apply, GeneralLinearGroup.val_swap, isNilpotent_iff, support_subset_support_matPolyEquiv, toLinAlgEquiv'_toMatrixAlgEquiv', ModularForm.prod_fintype_slash, kroneckerTMulAlgEquiv_apply, SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, matPolyEquiv_symm_map_eval, endVecAlgEquivMatrixEnd_symm_apply_apply, GeneralLinearGroup.map_apply, Ideal.matrix_strictMono_of_nonempty, instSMulCommClassMulOppositeForallOfIsScalarTower, AlgEquiv.mapMatrix_trans, toLinAlgEquiv'_one, SlashInvariantForm.vAdd_width_periodic, UpperHalfPlane.denom_one, isUnit_of_left_inverse, isUnit_exp, MatrixEquivTensor.right_inv, UpperHalfPlane.val_J, matPolyEquiv_eval, AlgEquiv.mopMatrix_symm_apply, ModularForm.slash_def, mulVec_surjective_iff_isUnit, UpperHalfPlane.instContinuousGLSMul, transposeAlgEquiv_symm_apply, ModularForm.is_invariant_one', EisensteinSeries.eisensteinSeriesSIF_apply, UpperHalfPlane.mul_smul', toLinAlgEquiv'_symm, instIsScalarTowerMulOppositeForallOfSMulCommClass, toLinearEquiv_kroneckerAlgEquiv, Module.diagonal_const_smul, IsHermitian.star_mul_self_mul_eq_diagonal, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing, GeneralLinearGroup.map_one, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, GeneralLinearGroup.map_mul, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite, SpecialLinearGroup.mapGL_coe_matrix, IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed, matPolyEquiv_symm_X, GeneralLinearGroup.coe_mul, pow_inv_comm', det_units_conj, aeval_self_charpoly, Module.Basis.toMatrix_reindex', map_pow, Subgroup.IsArithmetic.finiteIndex_comap, LinearMap.toMatrixAlgEquiv_apply', SpecialLinearGroup.det_mapGL, ModularForm.SL_slash_apply, disc_conj', SpecialLinearGroup.discreteSpecialLinearGroupIntRange, EisensteinSeries.eisSummand_SL2_apply, PosSemidef.sqrt_mul_self, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, isUnit_transpose, trace_units_conj', Ideal.matrix_bot, LinearMap.toMatrix_pow, ModularGroup.det_coe, Ideal.matrix_monotone, GeneralLinearGroup.val_inv_swap, UpperHalfPlane.denom_cocycle', Algebra.smulTower_leftMulMatrix_algebraMap_eq, ModularForm.coe_translate, adjugate_pow, UpperHalfPlane.neg_smul, GeneralLinearGroup.val_scalar_apply, LinearMap.toMatrixAlgEquiv_reindexRange, GeneralLinearGroup.map_id, Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, AffineBasis.isUnit_toMatrix, ModularForm.coe_trace, isUnit_diagonal, matPolyEquiv_coeff_apply_aux_2, zpow_neg_natCast, GLPos.coe_neg_GL, IsHermitian.conjStarAlgAut_star_eigenvectorUnitary, GeneralLinearGroup.coe_map_inv_mul_map, exp_units_conj, CongruenceSubgroup.IsCongruenceSubgroup.conjGL, Module.smul_def', Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL, matPolyEquiv_smul_one, rank_unit, LinearMap.toMatrixAlgEquiv_mul, matrixEquivTensor_apply, MatrixEquivTensor.toFunAlgHom_apply, GeneralLinearGroup.injective_upperRightHom, instIsArtinianRingMatrix, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, Represents.algebraMap, matPolyEquiv_eq_X_pow_sub_C, Algebra.leftMulMatrix_eq_repr_mul, ModularGroup.coeHom_apply, aeval_eq_aeval_mod_charpoly, Subgroup.strictWidthInfty_SL2Z, GeneralLinearGroup.IsParabolic.smul_eq_self_iff, sub_scalar_sq_eq_discr, kroneckerStarAlgEquiv_apply, IsAzumaya.matrix, SpecialLinearGroup.isInducing_toGL, toLpLinAlgEquiv_symm_apply, UpperHalfPlane.c_mul_im_sq_le_normSq_denom, Subgroup.IsArithmetic.discreteTopology, LinearMap.toMatrixAlgEquiv_transpose_apply, UpperHalfPlane.smulAux'_im, coe_units_zpow, PosDef.posDef_sqrt, piAlgEquiv_apply, Algebra.leftMulMatrix_apply, IsSimpleRing.exists_algEquiv_matrix_divisionRing, det_pow, op_smul_eq_vecMul, mvPolynomialX_mapMatrix_aeval, Subgroup.IsArithmetic.conj, SlashInvariantForm.coe_norm, algebraMap_matrix_apply, vecMul_surjective_iff_isUnit, toLinAlgEquiv_toMatrixAlgEquiv, toLinAlgEquiv_symm, LinearMap.toMatrixAlgEquiv_transpose_apply', kroneckerStarAlgEquiv_symm_apply, isPrimitive_iff, instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space, algebraMap_eq_diagonalRingHom, IsCusp.smul, SpecialLinearGroup.toGL_inj, MatrixModCat.fromMatrixLinear_apply_coe, GeneralLinearGroup.toLin_apply, mulVec_injective_iff_isUnit, isNilpotent_iff_forall_col, LinearMap.mapMatrixModule_comp_apply, linearIndependent_rows_iff_isUnit, fromBlocks_diagonal_pow, Subgroup.hasDetPlusMinusOne_iff_abs_det, PosSemidef.sqrt_eq_iff_eq_sq, SpecialLinearGroup.isEmbedding_mapGL, AlgHom.mulLeftRightMatrix.comp_inv, isUnit_comp_symm_iff, LinearMap.toMatrixAlgEquiv'_comp, UnitaryGroup.inv_apply, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, ModularForm.slash_apply, blockDiagonal'_pow, AlgEquiv.mapMatrix_apply, GLPos.coe_neg, GeneralLinearGroup.val_det_apply, UpperHalfPlane.petersson_slash, GeneralLinearGroup.fin_two_smul_prod
|
vecMul 📖 | CompOp | 105 mathmath: mulVec_transpose, PEquiv.vecMul_toMatrix_toPEquiv, single_vecMul, empty_vecMul, submatrix_vecMul_equiv, vecMul_vecMulVec, vecMul_neg, neg_vecMul_neg, updateRow_mul, coe_vecMulLinear, sum_vecMul, vecMul_diagonal, Algebra.traceMatrix_of_matrix_vecMul, ext_iff_vecMul, smul_vecMul, vecMulBilin_apply, vecMul_dotProduct_one_eq_one_rowStochastic, IsCoprime.vecMulSL, mul_apply_eq_vecMul, nonneg_vecMul_of_mem_rowStochastic, sub_vecMul, vecMul_fromRows, star_vecMul, nonneg_vecMul_of_mem_colStochastic, mulVec_vecMul, one_vecMul, vecMul_fromBlocks, vecMul_injective_of_isUnit, schur_complement_eq₂₂, vecMulLinear_apply, AffineBasis.toMatrix_vecMul_coords, vecMul_eq_sum, vecMulVec_mul, isRightRegular_iff_vecMul_injective, mulVec_replicateCol_eq_const, add_vecMul, vecMul_permMatrix, vecMul_ofNat, cons_mul, Algebra.discr_of_matrix_vecMul, CStarMatrix.toCLM_apply, EisensteinSeries.vecMul_SL2_mem_gammaSet, vecMul_conjTranspose_mul_self_eq_zero, zero_vecMul, schur_complement_eq₁₁, vec_vecMul_kronecker_of_commute, AffineBasis.toMatrix_inv_vecMul_toMatrix, vecMul_add, vecMul_injective, vecMul_surjective_iff_exists_left_inverse, vecMul_sum, replicateRow_vecMul, vecMul_diagonal_const, vecMul_vecMul, mulVec_conjTranspose, exists_vecMul_eq_zero_iff, toLinearMapRight'_apply, vec_vecMul_kronecker, vecMul_conjTranspose, one_vecMul_of_mem_doublyStochastic, dotProduct_vecMul_hadamard, vecMul_natCast, vecMul_injective_iff_isUnit, mem_colStochastic, Continuous.matrix_vecMul, vecMul_injective_of_invertible, vecMul_surjective_of_invertible, mem_doublyStochastic, vecMul_sub, vecMulᵣ_eq, EisensteinSeries.vecMulSL_gcd, mul_left_injective_iff_vecMul_injective, vecMul_fromCols, sumElim_vecMul_fromRows, cons_vecMul, SimpleGraph.adjMatrix_vecMul_apply, cons_vecMul_cons, vecMul_swap_apply, neg_vecMul, replicateCol_vecMul, EisensteinSeries.eisSummand_SL2_apply, vecMul_self_mul_conjTranspose_eq_zero, vecMul_updateCol, single_one_vecMul, vec_mul_eq_vecMul, vecMul_transpose, vecMul_mulVec, vecMul_cons, EisensteinSeries.eisensteinSeries_slash_apply, vecMul_intCast, vecMul_smul, vecMul_injective_iff, Module.Basis.toMatrix_map_vecMul, vecMul_zero, single_vecMul_diagonal, op_smul_eq_vecMul, one_vecMul_of_mem_colStochastic, vecMul_surjective_iff_isUnit, vecMul_swap, RingHom.map_vecMul, dotProduct_mulVec, det_smul_inv_vecMul_eq_cramer_transpose, vecMul_empty, star_mulVec, vecMul_one
|
vecMulVec 📖 | CompOp | 49 mathmath: vecMulVec_empty, smul_vecMulVec, vecMul_vecMulVec, diag_vecMulVec, posSemidef_vecMulVec_self_star, single_eq_single_vecMulVec_single, row_vecMulVec, vecMulVec_update, vecMulVec_add, rank_vecMulVec_le, Continuous.matrix_vecMulVec, LinearMap.toMatrix_innerₛₗ_apply, vecMulVec_mul, vecMulVec_eq, one_vecMulVec, LinearMap.toMatrix_smulRight, posSemidef_vecMulVec_star_self, vecMulVecBilin_apply_apply, transpose_vecMulVec, vecMulVec_one, vecMulVec_smul', InnerProductSpace.toMatrix_rankOne, vecMulVec_zero, update_vecMulVec, posSemidef_iff_eq_sum_vecMulVec, add_vecMulVec, charpoly_vecMulVec, trace_vecMulVec, toMatrix_innerSL_apply, vecMulVec_apply, vecMulVec_eq_zero, vecMulVec_mul_vecMulVec, cons_vecMulVec, LinearMap.toMatrix_toSpanSingleton, vecMulVec_cons, vecMulVec_neg, zero_vecMulVec, vecMulVec_mulVec, conjTranspose_vecMulVec, sub_vecMulVec, vecMulVec_smul, neg_vecMulVec, det_vecMulVec, empty_vecMulVec, mul_vecMulVec, InnerProductSpace.symm_toEuclideanLin_rankOne, rank_vecMulVec, vecMulVec_sub, col_vecMulVec
|
«term_*ᵥ_» 📖 | CompOp | — |
«term_ᵥ*_» 📖 | CompOp | — |