| Name | Category | Theorems |
|---|
add 📖 | CompOp | 180 mathmath: l2_opNorm_toEuclideanCLM, IsDiag.add, invOf_fromBlocks₂₂_eq, kroneckerTMulStarAlgEquiv_symm_apply, entryAddHom_apply, add_mul_mul_invOf_mul_eq_one, det_add_replicateCol_mul_replicateRow, cstar_nnnorm_def, vec_add, isParabolic_iff_exists, eval_det_add_X_smul, entryAddHom_eq_comp, add_mulVec, Polynomial.leadingCoeff_det_X_one_add_C, kronecker_add, single_add, toMvPolynomial_add, transposeAddEquiv_symm, RingCon.matrix_strictMono_of_nonempty, RingCon.matrix_top, LinearMap.toMatrixOrthonormal_reindex, toBlock_mul_eq_add, RingEquiv.mopMatrix_symm_apply, uniqueAddEquiv_apply, IsHermitian.add, RingEquiv.mopMatrix_apply, derivative_det_one_add_X_smul, TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r, add_apply, uniqueRingEquiv_apply, PosDef.posSemidef_add, PosDef.add, LinearMap.toMatrixOrthonormal_apply_apply, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, submatrix_add, det_add_mul, transpose_add, det_one_add_smul, MatrixEquivTensor.invFun_add, add_kronecker, mulVecLin_add, coe_ofAddEquiv_symm, inv_add_inv, exp_add_of_commute, transposeRingEquiv_symm_apply, piRingEquiv_apply, uniqueAddEquiv_symm_apply, isSemisimpleRing_iff_pi_matrix_divisionRing, conjTransposeLinearEquiv_apply, RingCon.ofMatrix_rel, vecMulVec_add, entryAddMonoidHom_eq_comp, of_add_of, AddEquiv.mapMatrix_trans, piRingEquiv_symm_apply, piLinearEquiv_apply, circulant_add, blockDiag_add, toEuclideanCLM_toLp, fromBlocks_mul_fromRows, RingCon.coe_ofMatrix_eq_relationMap, fromBlocks_add, BlockTriangular.add_iff_right, transpose_list_sum, AddEquiv.entryAddHom_comp_mapMatrix, LinearMap.toMatrixOrthonormal_symm_apply, replicateRow_add, SimpleGraph.IsSRGWith.matrix_eq, Polynomial.coeff_det_X_add_C_card, BlockTriangular.add, isSymm_add_transpose_self, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, compRingEquiv_symm_apply, det_one_add_X_smul, AddEquiv.mapMatrix_apply, add_mul_mul_invOf_mul_eq_one', ofLp_toEuclideanCLM, conjTranspose_list_sum, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, kroneckerTMulStarAlgEquiv_apply, transposeRingEquiv_apply, IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing, evalRingHom_mapMatrix_comp_compRingEquiv, PosSemidef.add, RingEquiv.map_det, add_mul_mul_mul_invOf_eq_one, RingCon.ofMatrix_rel', uniqueLinearEquiv_apply, entryAddMonoidHom_toAddHom, conjTransposeAddEquiv_apply, instContinuousAddMatrix, kroneckerTMul_add, piAddEquiv_symm_apply, coe_toEuclideanCLM_eq_toEuclideanLin, conjTransposeRingEquiv_symm_apply, LinearMap.toMatrixOrthonormal_apply, blockDiag'_add, invOf_add_mul_mul, add_mul, RingEquiv.mapMatrix_apply, mul_add, vecMul_add, add_hadamard, map_add, blockDiagonal'_add, transposeAddEquiv_apply, detp_smul_adjp, trace_list_sum, trace_add, IsSemisimpleModule.exists_end_ringEquiv, add_mul_mul_mul_invOf_eq_one', isHermitian_add_transpose_self, RingCon.matrix_injective, PosDef.add_posSemidef, RingCon.matrix_bot, blockDiagonal_add, uniqueRingEquiv_symm_apply, RingCon.matrix_apply_single, CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, add_kroneckerTMul, isHermitian_transpose_add_self, add_vecMulVec, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing, diag_add, detp_smul_add_adjp, det_mul_add_one_comm, isAddUnit_detp_smul_mul_adjp, coeff_det_one_add_X_smul_one, Represents.add, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, Polynomial.natDegree_det_X_add_C_le, uniqueLinearEquiv_symm_apply, diagonal_add, isSymm_transpose_add_self, hadamard_add, invOf_add_mul_mul', IsSimpleRing.exists_ringEquiv_matrix_divisionRing, kroneckerMap_add_right, det_one_add_replicateCol_mul_replicateRow, transposeAlgEquiv_symm_apply, diag_list_sum, AddEquiv.mapMatrix_symm, AddEquiv.mapMatrix_refl, SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes, conjTransposeRingEquiv_apply, compRingEquiv_apply, fromBlocks_multiply, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply, piLinearEquiv_symm_apply, RingEquiv.mapMatrix_refl, cstar_norm_def, fromCols_mul_fromRows, CStarMatrix.of_add_of, entryLinearMap_toAddHom, conjTranspose_add, RingCon.matrix_apply, RingEquiv.mapMatrix_trans, PEquiv.toMatrix_swap, derivative_det_one_add_X_smul_aux, kroneckerStarAlgEquiv_apply, mul_adjp_add_detp, coe_ofAddEquiv, fromCols_mul_fromBlocks, kroneckerMap_add_left, invOf_fromBlocks₁₁_eq, RingCon.matrix_monotone, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, conjTransposeAddEquiv_symm, transposeLinearEquiv_apply, IsSymm.add, piAddEquiv_apply, kroneckerStarAlgEquiv_symm_apply, det_one_add_mul_comm, compAddEquiv_symm_apply, compAddEquiv_apply, RingEquiv.mapMatrix_symm, Polynomial.coeff_det_X_add_C_zero, BlockTriangular.add_iff_left, replicateCol_add
|
addCommGroup 📖 | CompOp | 5 mathmath: AddMonoidHom.mapMatrix_sub, AddMonoidHom.mapMatrix_neg, finiteDimensional, LinearMap.mapMatrix_neg, LinearMap.mapMatrix_sub
|
addCommMonoid 📖 | CompOp | 576 mathmath: LinearMap.restrictScalars_toMatrix, LinearMap.SeparatingRight.toMatrix₂', LinearMap.charpoly_def, toLin_kronecker, toLin'_symm, SeparatingLeft.toBilin', LinearMap.detAux_def'', kroneckerTMulStarAlgEquiv_symm_apply, LinearMap.BilinForm.toMatrix_toBilin, Module.Basis.end_repr_apply, SeparatingRight.toLinearMap₂, BilinForm.toMatrix_symm, SimpleGraph.lapMatrix_toLinearMap₂', reindexLinearEquiv_trans, separatingRight_toLinearMap₂'_iff, Polynomial.toMatrix_sylvesterMap', toLinearMapRight'_mul, LinearMap.mapMatrix_zero, separatingRight_toLinearMap₂_iff, spectrum_toEuclideanLin, iSup_eigenspace_toLin'_diagonal_eq_top, LinearMap.mapMatrixLinear_apply, LinearMap.BilinForm.toMatrixAux_eq, toLinearMap₂'_comp, kroneckerTMulAlgEquiv_symm_single_tmul, LinearMap.toMatrix_apply', mem_pairSelfAdjointMatricesSubmodule, LinearMap.toMatrix₂_mul, conjTranspose_sum, LinearMap.entryLinearMap_comp_mapMatrix, repr_toLin, LinearEquiv.mapMatrix_apply, liftLinear_single, LinearMap.BilinForm.toMatrix_compRight, transposeLinearEquiv_symm, vec_sum, toLinearMap₂_toMatrix₂, LinearMap.toMatrix_one, summable_matrix_transpose, separatingRight_toBilin_iff, spectrum_toLpLin, sum_single_one, LinearMap.BilinForm.toMatrix'_symm, toLin_mul_apply, toMatrix_distrib_mul_action_toLinearMap, LinearMap.BilinForm.toMatrix'_apply, LinearMap.BilinForm.SeparatingRight.toMatrix, LinearMap.nondegenerate_toLinearMap₂'_of_det_ne_zero', Nondegenerate.toLinearMap₂, blockDiagonal_tsum, intrinsicStar_toLin', QuadraticMap.toMatrix'_comp, mulRightLinearMap_one, SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, star_dotProduct_toMatrix₂_mulVec, matrix_eq_sum_single, toBilin_symm, LinearMap.spectrum_toMatrix', Real.smul_map_diagonal_volume_pi, toMatrix_rotation, AlgHom.mulLeftRightMatrix.inv_comp, diagLinearMap_apply, diagonalLinearMap_apply, sum_sum_single, toLpLin_mul_same, LinearMap.toMatrix_baseChange, LinearMap.trace_eq_matrix_trace_of_finset, SeparatingLeft.toLinearMap₂', LinearMap.BilinForm.nondegenerate_toMatrix_iff, LinearMap.toMatrixₛₗ₂'_symm, trace_multiset_sum, LinearMap.rank_diagonal, rank_matrix_module, LinearMap.separatingRight_toMatrix₂'_iff, toEuclideanLin_apply, Algebra.toMatrix_lmul_eq, isAdjointPair_toLinearMap₂, liftLinear_singleLinearMap, LinearEquiv.mapMatrix_toLinearMap, liftLinear_comp_singleLinearMap, LinearMap.toMatrix_symm, toBilin_apply, LinearMap.toMatrix₂'_compl₁₂, Module.Basis.toLin_toMatrix, toLinearEquivRight'OfInv_symm_apply, toLin'_mul_apply, toLinearMapₛₗ₂'_single, nondegenerate_toBilin'_iff, LinearMap.toMatrix'_toLin', TensorProduct.toMatrix_assoc, toLinearMap₂'_apply', SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, LinearMap.toMatrix_id, LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec, MatrixEquivTensor.invFun_add, mul_reindexLinearEquiv_one, toAlgEquiv_kroneckerStarAlgEquiv, LinearMap.toMatrix_transpose, LinearMap.toMatrix₂_toLinearMapₛₗ₂, det_kroneckerMapBilinear, SpecialLinearGroup.toLin'_symm_to_linearMap, mem_skewAdjointMatricesSubmodule', vecMulBilin_apply, sum_apply, IsBaseChange.endHom_toMatrix, Real.map_matrix_volume_pi_eq_smul_volume_pi, conjTranspose_tsum, toAlgEquiv_kroneckerTMulStarAlgEquiv, toLinearMap₂'_apply, LinearMap.BilinForm.separatingLeft_toMatrix'_iff, ModularGroup.lcRow0Extend_symm_apply, Module.Basis.matrix_apply, conjTransposeLinearEquiv_apply, isNilpotent_toLin'_iff, toLinearEquiv'_symm_apply, LinearMap.BilinForm.mul_toMatrix'_mul, toLin_symm, BilinForm.mul_toMatrix_mul, Module.Basis.linearMap_apply, toLinearMap₂_compl₁₂, mem_pairSelfAdjointMatricesSubmodule', toLinearMapₛₗ₂'_symm, summable_matrix_diagonal, MatrixEquivTensor.toFunBilinear_apply, LinearMap.toBilin'Aux_toMatrixAux, piLinearEquiv_apply, LinearMap.toMatrix₂_compl₂, toLpLin_symm_pow, LinearEquiv.mapMatrix_symm, instIsStablyFiniteRing, toLinearMapₛₗ₂'_aux_eq, MatrixEquivTensor.invFun_algebraMap, linfty_opNNNorm_toMatrix, Algebra.traceForm_toMatrix, toLin_scalar, toBilin'Aux_toMatrixAux, BilinForm.dotProduct_toMatrix_mulVec, toLpLin_one, LinearMap.isPosSemidef_iff_posSemidef_toMatrix, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, singleLinearMap_apply, piLp_ofLp_toEuclideanLin, LinearMap.BilinForm.toMatrix_apply, Summable.matrix_diagonal, lieEquivMatrix'_apply, det_sum_le, BilinForm.toMatrix_toBilin, SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux, LinearMap.minpoly_toMatrix', LinearMap.toMatrix₂_comp, SeparatingRight.toLinearMap₂', toLpLin_pow, kroneckerAlgEquiv_apply, LinearMap.BilinForm.separatingRight_toMatrix'_iff, isUnit_toLin'_iff, toLin'_mul, ModularGroup.lcRow0Extend_apply, LinearMap.isNilpotent_toMatrix_iff, LinearMap.BilinForm.dotProduct_toMatrix_mulVec, LinearMap.det_eq_det_toMatrix_of_finset, LinearMap.toMatrix_reindexRange, ofLp_toLpLin, toMatrix₂Aux_toLinearMap₂'Aux, toBilin'_symm, LinearMap.toMatrix_smulBasis_left, LinearMap.det_toLin', kroneckerMapBilinear_apply_apply, rank_eq_finrank_range_toLin, toLinearMapRight'_mul_apply, BilinForm.toMatrix_comp, reindexLinearEquiv_one, toLin_mul, toLin_pow, toLin_self, kroneckerTMulLinearEquiv_one, mulRightLinearMap_zero_eq_zero, LinearMap.separatingLeft_toMatrix₂'_iff, summable_matrix_conjTranspose, hasEigenvector_toLin'_diagonal, nondegenerate_toBilin'_iff_nondegenerate_toBilin, reindexLinearEquiv_comp, toLinearMapₛₗ₂'_toMatrix', LinearMap.toMatrix'_algebraMap, PiToModule.fromMatrix_apply_single_one, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, BilinearForm.toMatrixAux_eq, SeparatingLeft.toBilin, charpoly_toLin, LinearMap.toMatrixOrthonormal_symm_apply, LinearMap.toMatrix_mulVec_repr, LinearMap.toMatrix_innerₛₗ_apply, exp_sum_of_commute, conjTransposeLinearEquiv_symm, toLin_apply_eq_zero_iff, nondegenerate_toBilin_iff, toLin'_reindex, transpose_multiset_sum, PosSemidef.toLinearMap₂'_zero_iff, LinearMap.BilinForm.toMatrix'_compLeft, toLinearMapₛₗ₂_apply, convex_colStochastic, diag_multiset_sum, Module.Basis.end_apply, sum_single_ofNat, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, compRingEquiv_symm_apply, commute_mulLeftLinearMap_mulRightLinearMap, Nondegenerate.toBilin, LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero, trace_sum, LinearMap.toMatrix'_apply, toLpLin_toLp, apply_eq_dotProduct_toMatrix₂_mulVec, kroneckerLinearEquiv_symm_kronecker, LinearMap.BilinForm.separatingRight_toMatrix_iff, summable_matrix_blockDiagonal', LinearMap.BilinForm.SeparatingLeft.toMatrix', LinearEquiv.mapMatrix_refl, ker_toLin_eq_bot, IntrinsicStar.isSelfAdjoint_toLin'_iff, pow_mulLeftLinearMap, LinearMap.toMatrix'_symm, LinearMap.mapMatrix_smul, mulRightLinearMap_eq_zero_iff, linearMap_toMatrix_mul_basis_toMatrix, kroneckerTMulAlgEquiv_symm_apply, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, LinearMap.toMatrix_transpose_apply, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, kroneckerTMulStarAlgEquiv_apply, toMatrix_dualTensorHom, range_toLin', RootPairing.GeckConstruction.span_range_h_le_range_diagonal, LinearMap.mul_toMatrix', liftLinear_apply, evalRingHom_mapMatrix_comp_compRingEquiv, pow_mulRightLinearMap, LinearMap.toMatrix_smulBasis_right, toLpLin_symm_id, range_toLin_eq_top, HasSum.matrix_diagonal, toLin_finTwoProd_apply, isPositive_toEuclideanLin_iff, CStarMatrix.ofMatrix_eq_ofMatrixL, LinearMap.mul_toMatrix₂, mem_skewAdjointMatricesLieSubalgebra, kroneckerTMulLinearEquiv_mul, QuadraticMap.discr_comp, Module.Basis.linearMap_repr_apply, kroneckerTMulLinearEquiv_symm_kroneckerTMul, traceLinearMap_apply, dualNumberEquiv_symm_apply, LinearMap.toMatrix'_mul, mul_basis_toMatrix, proj_comp_diagLinearMap, LinearMap.toMatrix_algebraMap, LinearMap.spectrum_toMatrix, LinearMap.SeparatingRight.toMatrix₂, isUnit_toLin_iff, uniqueLinearEquiv_apply, diagonal_toLin', charpoly_toLin', LinearMap.BilinForm.toMatrix_symm, toLinearMap₂'_toMatrix', toLinearMapₛₗ₂'_apply, toLin'_pow, LinearMap.BilinForm.SeparatingLeft.toMatrix, l2_opNNNorm_def, apply_eq_star_dotProduct_toMatrix₂_mulVec, LinearMap.toMatrix_mul, LinearMap.toMatrix₂_compl₁₂, minpoly_toLin', BilinForm.toMatrix_compRight, LinearMap.BilinForm.nondegenerate_toMatrix'_iff, LinearMap.toMatrix₂_toLinearMap₂, LinearMap.detAux_def', LinearMap.toMatrix_transpose_apply', LinearMap.toMatrix'_intrinsicStar, compLinearEquiv_symm_apply, IsBaseChange.linearMapLeftRightHom_toMatrix, LinearMap.BilinForm.toMatrixAux_apply, SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, Module.finrank_matrix, toLinOfInv_symm_apply, LinearMap.toMatrix_smulRight, kroneckerTMulLinearEquiv_tmul, LinearMap.toMatrix₂Aux_eq, LinearMap.mapMatrix_comp, vecMulVecBilin_apply_apply, isAdjointPair_toLinearMap₂', toLin'_apply', LinearMap.toMatrix₂_symm, ker_toLin'_eq_bot_iff, LinearMap.SeparatingLeft.toMatrix₂, LinearMap.toMatrix'_toLinearMap₂', BilinForm.toMatrix_mul_basis_toMatrix, LinearMap.BilinForm.mul_toMatrix', toLinearMap₂_symm, coe_toEuclideanCLM_eq_toEuclideanLin, LinearMap.toMatrixRight'_id, LinearMap.minpoly_toMatrix, matrixEquivTensor_apply_single, nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂, LinearEquiv.mapMatrix_trans, LinearMap.toMatrixOrthonormal_apply, MatrixEquivTensor.invFun_smul, sum_mul, Algebra.toMatrix_lmul', mem_skewAdjointMatricesSubmodule, ker_diagonal_toLin', matrixEquivTensor_apply_symm, toBilin'_apply, LinearMap.toMatrix_prodMap, toLin_apply, toLin'_one, MatrixEquivTensor.left_inv, posDef_sum, doublyStochastic_eq_convexHull_permMatrix, reindexLinearEquiv_mul, toLin_conjTranspose, mulRightLinearMap_apply, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, rank_matrix_module', trace_toLin'_eq, vecMul_sum, toLin'OfInv_symm_apply, Orientation.rotation_eq_matrix_toLin, LinearEquiv.isUnit_det, mem_selfAdjointMatricesSubmodule, Algebra.traceMatrix_of_basis, spectrum_toLin, LinearMap.toMatrix'_comp, toLinearEquiv'_apply, LinearMap.isUnit_toMatrix'_iff, toBilin_toMatrix, nondegenerate_toLinearMap₂_iff, reindexLinearEquiv_apply, toBilin'_comp, isHermitian_iff_isSymmetric, LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal', Module.Free.matrix, Module.Basis.end_repr_symm_apply, InnerProductSpace.toMatrix_rankOne, rank_matrix', ext_linearMap_iff, LinearMap.mul_toMatrix₂_mul, transpose_tsum, toEuclideanLin_conjTranspose_eq_adjoint, stdBasis_eq_single, LinearMap.toMatrix'_id, toLinearMapₛₗ₂_symm, LinearMap.BilinForm.mul_toMatrix_mul, posSemidef_sum, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix, LinearMap.nondegenerate_toMatrix₂'_iff, LinearMap.BilinForm.toMatrix'_comp, LinearMap.mapMatrix_apply, mulLinearMap_apply_apply, toLinearMapRight'_apply, LinearMap.BilinForm.toMatrix_mul, rank_matrix, posSemidef_iff_eq_sum_vecMulVec, ofLp_toEuclideanLin_apply, toLinearMap₂_apply, LinearMap.nondegenerate_toLinearMap₂'_iff_det_ne_zero, mulVecBilin_apply, lieEquivMatrix'_symm_apply, proj_diagonal, extremePoints_doublyStochastic, LinearMap.isUnit_toMatrix_iff, LinearMap.BilinForm.toMatrix_compLeft, LinearMap.trace_eq_matrix_trace, BilinForm.toMatrix_apply, linfty_opNorm_toMatrix, toBilin'_apply', toLinearMap₂'_single, LinearMap.separatingRight_toLinearMap₂'_of_det_ne_zero', mulLeftLinearMap_one, LinearMap.BilinForm.mul_toMatrix, reindexLinearEquiv_symm, SpecialLinearGroup.toLin'_to_linearMap, LinearMap.mul_toMatrix₂'_mul, LinearMap.toMatrix₂'_mul, instIsOrderedAddMonoid, Algebra.toMatrix_lsmul, toMatrix_innerSL_apply, separatingLeft_toLinearMap₂'_iff, LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero', BilinForm.toMatrix_mul, LinearMap.toMatrix_comp, ModularGroup.tendsto_lcRow0, kroneckerMapBilinear_mul_mul, separatingLeft_toBilin'_iff, kroneckerAlgEquiv_symm_apply, trace_toLin_eq, LinearMap.toMatrix₂_mul_basis_toMatrix, Module.Basis.toMatrix_eq_toMatrix_constr, det_reindexLinearEquiv_self, toLinOfInv_apply, mulRightLinearMap_mul, toBilin'Aux_eq, LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix', toLin_finTwoProd_toContinuousLinearMap, LinearMap.mapMatrix_id, kroneckerTMulBilinear_apply, uniqueLinearEquiv_symm_apply, sum_single_intCast, conjTranspose_multiset_sum, toLinearEquivRight'OfInv_apply, hasEigenvalue_toLin'_diagonal_iff, LinearMap.toMatrix'_toLinearMapₛₗ₂', toLpLin_mul, convex_rowStochastic, toLin'_submatrix, separatingLeft_toLinearMap₂_iff, toLin_toMatrix, LinearMap.toMatrix₂_apply, PiToModule.fromMatrix_apply, toEuclideanLin_apply_piLp_toLp, Polynomial.toMatrix_sylvesterMap, dualNumberEquiv_apply, separatingRight_toBilin'_iff, toLin_finTwoProd, SpecialLinearGroup.toLin_equiv.toLinearMap_eq, Module.Basis.linearMap_repr_symm_apply, kroneckerTMulAlgEquiv_apply, LinearMap.nondegenerate_toMatrix₂_iff, trace_kroneckerMapBilinear, LinearMap.mapMatrix_add, toLin_one, toLin_transpose, Complex.toMatrix_conjAe, BilinForm.mul_toMatrix, MatrixEquivTensor.right_inv, toLpLin_symm_comp, toLinearMapₛₗ₂_apply_basis, convex_doublyStochastic, LinearMap.toMatrix_toSpanSingleton, LinearMap.toMatrix₂_symm', mulLeftLinearMap_zero_eq_zero, sum_single_natCast, LinearMap.Nondegenerate.toMatrix₂', MatrixEquivTensor.invFun_zero, Nondegenerate.toBilin', LinearMap.toMatrix_singleton, LinearMap.BilinForm.toMatrix'_mul, sum_mulVec, LinearMap.toMatrix₂'_compl₂, entryLinearMap_apply, sum_single_eq_diagonal, toLinearEquiv_kroneckerAlgEquiv, det_sum_smul_le, nondegenerate_toLinearMap₂'_iff, LinearMap.separatingRight_toMatrix₂_iff, reindexLinearEquiv_refl_refl, LinearMap.separatingLeft_toMatrix₂_iff, Module.Finite.matrix, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, AddMonoidHom.mapMatrix_add, LinearMap.BilinForm.toMatrix'_toBilin', compRingEquiv_apply, LinearMap.det_toMatrix', separatingLeft_toBilin_iff, LinearMap.Nondegenerate.toMatrix₂, toLin'OfInv_apply, mulLeftLinearMap_eq_zero_iff, LinearMap.BilinForm.Nondegenerate.toMatrix', LinearMap.toMatrix_basis_equiv, reindexLinearEquiv_comp_apply, SeparatingRight.toBilin', BilinForm.apply_eq_dotProduct_toMatrix_mulVec, range_diagonal, piLinearEquiv_symm_apply, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, diag_sum, mulLeftLinearMap_apply, BilinForm.toMatrix_compLeft, maxGenEigenspace_toLin_diagonal_eq_eigenspace, LinearMap.toMatrix₂'_comp, mulLeftLinearMap_mul, toLinearMap₂_apply_basis, coe_ofLinearEquiv_symm, LinearMap.toMatrix_pow, diagonal_tsum, mem_selfAdjointMatricesSubmodule', LinearMap.BilinForm.toMatrix_comp, SpecialLinearGroup.toLin'_symm_apply, ModularGroup.lcRow0_apply, LinearMap.toMatrix'_one, iSup_eigenspace_toLin_diagonal_eq_top, basis_toMatrix_mul_linearMap_toMatrix, LinearMap.toMatrixₛₗ₂'_apply, toLinearMapRight'_one, maxGenEigenspace_toLin'_diagonal_eq_eigenspace, Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix, LinearEquiv.entryLinearMap_comp_mapMatrix, toLpLin_apply, entryLinearMap_toAddHom, toLin'_apply, blockDiagonal'_tsum, LinearMap.BilinForm.SeparatingRight.toMatrix', LinearMap.toMatrix_adjoint, compLinearEquiv_apply, LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero, LinearMap.BilinForm.Nondegenerate.toMatrix, l2_opNorm_def, matrixEquivTensor_apply, toEuclideanLin_toLp, MatrixEquivTensor.toFunAlgHom_apply, entryLinearMap_toAddMonoidHom, LinearMap.det_toMatrix, Algebra.traceForm_toMatrix_powerBasis, minpoly_toLin, basis_toMatrix_mul, toLin'_toMatrix', Submodule.coe_matrix, LinearMap.det_toLin, LinearMap.posSemidef_toMatrix_iff, coe_ofLinearEquiv, LinearMap.mapMatrix_neg, LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero', LinearMap.SeparatingLeft.toMatrix₂', TensorProduct.toMatrix_comm, LinearMap.toMatrix₂'_apply, kroneckerStarAlgEquiv_apply, separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂, LinearMap.BilinForm.separatingLeft_toMatrix_iff, Real.volume_preserving_transvectionStruct, toBilin'_toMatrix', toLinearMapₛₗ₂_toMatrix₂, LinearMap.toMatrix'_mulVec, SeparatingLeft.toLinearMap₂, hasEigenvector_toLin_diagonal, LinearMap.separatingRight_toLinearMap₂'_iff_det_ne_zero, dotProduct_toMatrix₂_mulVec, entryLinearMap_eq_comp, diagonal_comp_single, exists_eq_sum_perm_of_mem_doublyStochastic, LinearMap.traceAux_def, Algebra.leftMulMatrix_apply, InnerProductSpace.symm_toEuclideanLin_rankOne, LinearMap.BilinForm.toMatrix'_compRight, rank_matrix'', SeparatingRight.toBilin, transposeLinearEquiv_apply, LinearMap.toMatrix_apply, TensorProduct.toMatrix_map, rank_vecMulVec, transpose_sum, LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrixRight'_comp, kroneckerStarAlgEquiv_symm_apply, mul_sum, summable_matrix_blockDiagonal, LinearMap.mapMatrix_sub, toBilin_comp, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj, SimpleGraph.mem_ker_toLin'_lapMatrix_of_connectedComponent, ModularGroup.smul_eq_lcRow0_add, LinearMap.det_toMatrix_eq_det_toMatrix, SpecialLinearGroup.toLin'_apply, Nondegenerate.toLinearMap₂', AlgHom.mulLeftRightMatrix.comp_inv, separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂, LinearMap.toMatrix₂Aux_apply, LinearMap.charpoly_toMatrix, LinearMap.toLinearMap₂'Aux_toMatrix₂Aux, LinearMap.isSymm_iff_isHermitian_toMatrix, toBilin'_single, LinearMap.toMatrix_toLin, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, toLinearEquiv_apply, hasEigenvalue_toLin_diagonal_iff, spectrum_toLin', kroneckerLinearEquiv_tmul
|
addCommSemigroup 📖 | CompOp | 1 mathmath: LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle
|
addGroup 📖 | CompOp | 13 mathmath: RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, RootPairing.GeckConstruction.lie_h_e, conjTranspose_zsmul, exp_zsmul, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', AddSubgroup.coe_matrix, instIsTopologicalAddGroupMatrix, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, instIsUniformAddGroup, RootPairing.GeckConstruction.lie_h_f, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', LieAlgebra.SpecialLinear.sl_non_abelian
|
addMonoid 📖 | CompOp | 9 mathmath: natCast_kronecker, kronecker_natCast, exp_nsmul, SimpleGraph.IsSRGWith.matrix_eq, isAddUnit_detp_smul_mul_adjp, isAddUnit_iff, entryLinearMap_toAddMonoidHom, AddMonoidHom.mapMatrix_smul, conjTranspose_nsmul
|
addSemigroup 📖 | CompOp | — |
addZeroClass 📖 | CompOp | 38 mathmath: AddMonoidHom.mapMatrix_comp, AddMonoidHom.mapMatrix_id, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, Semiring.smulCommClass, AddMonoidHom.mapMatrix_zero, diagLinearMap_apply, diagonalLinearMap_apply, addMonoidHomMulLeft_apply, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, Subring.coe_matrix, entryAddMonoidHom_eq_comp, addMonoidHomMulRight_apply, AddMonoidHom.entryAddMonoidHom_comp_mapMatrix, singleAddMonoidHom_apply, AddMonoidHom.mapMatrix_sub, entryAddMonoidHom_apply, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', evalAddMonoidHom_comp_diagAddMonoidHom, Subalgebra.coe_matrix, entryAddMonoidHom_toAddHom, diagonalAddMonoidHom_apply, AddMonoidHom.mapMatrix_neg, diagAddMonoidHom_apply, blockDiagonal'AddMonoidHom_apply, AddMonoidHom.mapMatrix_apply, blockDiag'AddMonoidHom_apply, traceAddMonoidHom_apply, Semiring.isScalarTower, Subsemiring.coe_matrix, blockDiagAddMonoidHom_apply, AddMonoidHom.mapMatrix_add, blockDiagonalAddMonoidHom_apply, AddSubmonoid.coe_matrix, entryLinearMap_toAddMonoidHom, mulVec.addMonoidHomLeft_apply, AddMonoidHom.mapMatrix_smul, ext_addMonoidHom_iff, LieAlgebra.SpecialLinear.sl_non_abelian
|
col 📖 | CompOp | 29 mathmath: col_apply, mulVec_single_one, col_transpose, IsHermitian.eigenvectorUnitary_col_eq, linearIndependent_cols_of_isUnit, cRank_toNat_eq_finrank, linearIndependent_cols_of_det_ne_zero, basis_toMatrix_basisFun_mul, eRank_toNat_eq_finrank, col_submatrix, row_transpose, mul_single_eq_updateCol_zero, range_mulVecLin, range_toLin', col_def, linearIndependent_cols_iff_isUnit, col_eq_transpose, col_diagonal, col_submatrix_eq_comp, of_col, col_apply', mulVec_injective_iff, mulVec_single, col_map, linearIndependent_cols_of_invertible, rank_eq_finrank_span_cols, ext_col_iff, isNilpotent_iff_forall_col, col_vecMulVec
|
distribMulAction 📖 | CompOp | 4 mathmath: kroneckerTMulStarAlgEquiv_symm_apply, LinearMap.mapMatrix_smul, kroneckerTMulStarAlgEquiv_apply, AddMonoidHom.mapMatrix_smul
|
inhabited 📖 | CompOp | — |
map 📖 | CompOp | 150 mathmath: LinearMap.restrictScalars_toMatrix, IsSymm.map, fromCols_map, det_det, kroneckerMap_map_left, BlockTriangular.map, LinearEquiv.mapMatrix_apply, eval_det_add_X_smul, charpoly_map, RootPairing.Base.cartanMatrix_map_abs, Polynomial.leadingCoeff_det_X_one_add_C, RingHom.mapMatrix_apply, map_swap, frobenius_nnnorm_map_eq, kroneckerTMul_assoc', intrinsicStar_toLin', map_zero, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, RingEquiv.mopMatrix_symm_apply, map_mul_natCast, star_vec, blockDiagonal'_map, LinearMap.toMatrix_baseChange, RingHom.map_matrix_mul, RingEquiv.mopMatrix_apply, derivative_det_one_add_X_smul, Equiv.mapMatrix_apply, PEquiv.map_toMatrix, AddMonoidHom.map_trace, inv_denom_smul_num, Algebra.Norm.Transitivity.comp_det_mul_pow, Algebra.traceMatrix_of_matrix_vecMul, det_one_add_smul, map_toSquareBlock, det_kroneckerMapBilinear, map_mul_ratCast, IsBaseChange.endHom_toMatrix, piRingEquiv_apply, map_circulant, toMvPolynomial_map, map_id', kroneckerMap_map_right, map_injective, comp_transpose, MatrixEquivTensor.toFunBilinear_apply, frobenius_norm_map_eq, map_updateRow, MatrixEquivTensor.invFun_algebraMap, AlgEquiv.mopMatrix_apply, Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans, map_apply, map_sub, map_one, map_algebraMap, kroneckerMap_diagonal_right, norm_map_eq, blockDiagonal_map, den_map_intCast, charmatrix_fromBlocks, Int.cast_det, AlgHom.mapMatrix_apply, transpose_conjTranspose, Polynomial.coeff_det_X_add_C_card, map_id, det_one_add_X_smul, AddEquiv.mapMatrix_apply, blockDiag_map, Algebra.discr_of_matrix_mulVec, transpose_map, diagonal_kroneckerTMul, Rat.cast_det, Continuous.matrix_map, map_single, Algebra.discr_of_matrix_vecMul, den_map_natCast, num_map_intCast, num_map_natCast, LinearMap.toMatrix'_intrinsicStar, map_op_smul', IsBaseChange.linearMapLeftRightHom_toMatrix, fromBlocks_map, IsHermitian.map, matPolyEquiv_map_C, Algebra.Norm.Transitivity.eval_zero_comp_det, row_map, RingEquiv.mapMatrix_apply, matrixEquivTensor_apply_symm, RingHom.map_mulVec, AddMonoidHom.mapMatrix_apply, kroneckerMap_map, map_add, NumberField.conj_basisMatrix, matPolyEquiv_symm_C, map_natCast, diag_map, IsDiag.map, LinearMap.mapMatrix_apply, Topology.IsInducing.matrix_map, map_mul_intCast, fromRows_map, matPolyEquiv_eval_eq_map, GeneralLinearGroup.coe_map_mul_map_inv, comp_map_map, map_map, Topology.IsOpenEmbedding.matrix_map, coeff_det_one_add_X_smul_one, Polynomial.natDegree_det_X_add_C_le, Topology.IsEmbedding.matrix_map, GeneralLinearGroup.val_map_apply, map_intCast, blockDiag'_map, charmatrix_map, map_smul', Algebra.traceMatrix_of_matrix_mulVec, mvPolynomialX_map_eval₂, kroneckerTMul_diagonal, matPolyEquiv_symm_map_eval, AlgEquiv.mopMatrix_symm_apply, comp_symm_transpose, map_smulₛₗ, conjTranspose_transpose, SpecialLinearGroup.coe_matrix_coe, map_smul, map_pow, map_ofNat, map_updateCol, kroneckerTMul_assoc, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, submatrix_map, diagonal_map, map_mul, piEquiv_apply, comp_map_transpose, conjTranspose_map, col_map, GeneralLinearGroup.coe_map_inv_mul_map, MatrixEquivTensor.toFunAlgHom_apply, derivative_det_one_add_X_smul_aux, nnnorm_map_eq, vec_map, Module.Basis.toMatrix_map_vecMul, Topology.IsClosedEmbedding.matrix_map, piAlgEquiv_apply, kroneckerMap_diagonal_left, CStarMatrix.map_map, piAddEquiv_apply, Polynomial.coeff_det_X_add_C_zero, RingHom.map_vecMul, Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans, AlgEquiv.mapMatrix_apply
|
mulAction 📖 | CompOp | — |
neg 📖 | CompOp | 60 mathmath: circulant_neg, invOf_fromBlocks₂₂_eq, Algebra.Norm.Transitivity.polyToMatrix_cornerAddX, LieAlgebra.Orthogonal.mem_so, SymplecticGroup.coe_inv, inv_fromBlocks_zero₁₂_of_isUnit_iff, vec_neg, vecMul_neg, exp_neg, neg_vecMul_neg, neg_mulVec_neg, isDiag_neg_iff, IsHermitian.neg, blockDiagonal'_neg, neg_of, neg_apply, num_neg, blockDiagonal_neg, mul_neg, BlockTriangular.neg, J_squared, fromRows_neg, charmatrix_fromBlocks, fromBlocks_neg, J_transpose, IsDiag.neg, transpose_neg, neg_mulVec, blockDiag'_neg, RootPairing.GeckConstruction.ω_mul_h, invOf_fromBlocks_zero₁₂_eq, LieAlgebra.Orthogonal.s_as_blocks, SymplecticGroup.inv_left_mul_aux, det_neg, diag_neg, instContinuousNegMatrix, inv_fromBlocks_zero₂₁_of_isUnit_iff, J_inv, IsSymm.neg, SymplecticGroup.neg_mem, conjTranspose_neg, CStarMatrix.neg_of, invOf_fromBlocks_zero₂₁_eq, diagonal_neg, det_neg_eq_smul, vecMulVec_neg, SpecialLinearGroup.coe_neg, neg_mul, neg_vecMulVec, trace_neg, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, den_neg, blockDiag_neg, fromCols_neg, ModularGroup.S_mul_S_eq, invOf_fromBlocks₁₁_eq, RootPairing.GeckConstruction.lie_e_f_mul_ω, SymplecticGroup.inv_eq_symplectic_inv, submatrix_neg, GLPos.coe_neg
|
of 📖 | CompOp | 135 mathmath: vecMulVec_empty, replicateCol_cons, ZSpan.volume_real_fundamentalDomain, mul_mul_left, adjugate_fin_two, diagonal_vec3, CartanMatrix.C_two, diagonal_fin_two, toSquareBlock_def, NumberField.Units.regOfFamily_eq_det, CartanMatrix.D_four, mul_val_succ, diagonal_vec1, sum_sum_single, vandermonde_succ, det_eval_matrixOfPolynomials_eq_det_vandermonde, vec_of, hadamard_of_one, coe_ofAddEquiv_symm, diagonal_vec2, GeneralLinearGroup.upperRightHom_apply, uniqueEquiv_symm_apply, uniqueAddEquiv_symm_apply, adjugate_fin_three, natCast_fin_three, CartanMatrix.D_three, neg_of, eta_fin_three, PowerBasis.leftMulMatrix, NumberField.Units.regulator_eq_det, replicateRow_empty, of_add_of, piRingEquiv_symm_apply, smul_of, replicateRow_cons, NumberField.Units.finrank_mul_regOfFamily_eq_det, ZSpan.volume_fundamentalDomain, basis_toMatrix_basisFun_mul, natCast_fin_two, eta_fin_two, charpoly.univ_coeff_eval₂Hom, transpose_empty_cols, of_one_hadamard, ModularGroup.coe_T_inv, of_zero, CartanMatrix.B_two, adjugate_fin_three_of, mul_mul_right, ofNat_fin_three, ofNat_fin_two, cons_transpose, SimpleGraph.incMatrix_mul_transpose, of_apply, exteriorPower.ιMultiDual_apply_ιMulti, toLin_finTwoProd_apply, diagonal_fin_one, exteriorPower.pairingDual_ιMulti_ιMulti, val_planeConformalMatrix, dualNumberEquiv_symm_apply, cons_mul, SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero, CartanMatrix.A_three, col_eq_transpose, piAddEquiv_symm_apply, trace_fin_one_of, replicateRow_mul_replicateCol, Algebra.leftMulMatrix_complex, adjugate_def, Orientation.rotation_eq_matrix_toLin, NumberField.Units.abs_det_eq_abs_det, CartanMatrix.A_two, CartanMatrix.D_two, uniqueRingEquiv_symm_apply, exteriorPower.alternatingMapToDual_apply_ιMulti, piEquiv_symm_apply, mul_empty, piAlgEquiv_symm_apply, of_mem_specialOrthogonalGroup_fin_two_iff, PiLp.basis_toMatrix_basisFun_mul, tail_transpose, row_eq_self, det_mul_column, one_fin_three, toLin_finTwoProd_toContinuousLinearMap, toSquareBlockProp_def, of_symm_single, single_eq_of_single_single, matrixOfPolynomials_blockTriangular, uniqueAlgEquiv_symm_apply, of_col, empty_mul, trace_fin_three_of, det_matrixOfPolynomials, of_row, of_symm_apply, dualNumberEquiv_apply, toLin_finTwoProd, mul_fin_two, det_mul_row, Complex.toMatrix_conjAe, cons_vecMul, det_fin_one_of, UpperHalfPlane.val_J, vecMulVec_cons, ModularGroup.coe_T, cons_vecMul_cons, charpoly.univ_map_eval₂Hom, det_fin_two_of, diagonal_unique, cons_mulVec, mul_fin_three, SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes, of_sub_of, CartanMatrix.A_one, coe_ofLinearEquiv_symm, ModularGroup.coe_T_zpow, diagonal_fin_three, NumberField.Units.finrank_mul_regulator_eq_det, transpose_empty_rows, NumberField.Units.regulator_eq_det', ModularGroup.coe_S, vecMul_cons, mulVec_cons, head_transpose, Algebra.traceForm_toMatrix_powerBasis, coe_ofLinearEquiv, Set.matrix_eq_pi, coe_ofAddEquiv, NumberField.Units.regOfFamily_eq_det', eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials, adjugate_fin_two_of, one_fin_two, trace_fin_two_of, Pi.basisFun_det_apply, ZLattice.covolume_eq_det
|
ofAddEquiv 📖 | CompOp | 4 mathmath: entryAddHom_eq_comp, coe_ofAddEquiv_symm, entryAddMonoidHom_eq_comp, coe_ofAddEquiv
|
reindex 📖 | CompOp | 62 mathmath: natCast_kronecker, reindex_mem_doublyStochastic, reindex_mem_doublyStochastic_iff, abs_det_reindex, one_kronecker, Polynomial.sylvester_comm, reindex_mem_colStochastic_iff, charmatrix_reindex, kroneckerMap_reindex_right, LinearMap.toMatrixOrthonormal_reindex, kroneckerMap_assoc₁, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, kroneckerMap_reindex, updateCol_reindex, Algebra.traceMatrix_reindex, eRank_reindex, reindex_mem_rowStochastic_iff, reindex_apply, inv_reindex, updateRow_reindex, CartanMatrix.D_three', comp_toSquareBlock, cramer_reindex, reindex_isTotallyUnimodular, kroneckerMap_reindex_left, toLin'_reindex, adjugate_reindex, det_reindex, reindexLieEquiv_apply, diagonal_kroneckerTMul, CStarMatrix.reindexₐ_apply, reindex_updateRow, cRank_reindex, rank_reindex, lift_cRank_reindex, kronecker_assoc, NumberField.conj_basisMatrix, reindexLinearEquiv_apply, CStarMatrix.reindexₗ_apply, diagonal_kronecker, det_reindex_self, IsTotallyUnimodular.reindex, reindex_symm, reindex_refl_refl, kroneckerMap_assoc, Continuous.matrix_reindex, reindex_mem_rowStochastic, reindex_mem_colStochastic, reindexAlgEquiv_apply, reindex_trans, Polynomial.toMatrix_sylvesterMap, ofNat_kronecker, mulVecLin_reindex, comp_diagonal, charpoly_reindex, kroneckerTMul_assoc, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, transpose_reindex, reindex_updateCol, kroneckerMap_diagonal_left, blockTriangular_reindex_iff, conjTranspose_reindex
|
row 📖 | CompOp | 23 mathmath: row_def, single_vecMul, col_transpose, range_vecMulLinear, ext_row_iff, linearIndependent_rows_of_invertible, isNilpotent_iff_forall_row, row_vecMulVec, row_diagonal, linearIndependent_rows_of_isUnit, row_apply', row_transpose, rank_eq_finrank_span_row, row_map, single_mul_eq_updateRow_zero, row_eq_self, of_row, row_submatrix_eq_comp, row_apply, single_one_vecMul, vecMul_injective_iff, linearIndependent_rows_iff_isUnit, row_submatrix
|
smul 📖 | CompOp | 161 mathmath: l2_opNorm_toEuclideanCLM, circulant_smul, kroneckerTMulStarAlgEquiv_symm_apply, frobeniusIsBoundedSMul, smul_vecMulVec, isCentralScalar, hadamard_smul, cstar_nnnorm_def, mul_mul_left, diag_smul, eval_det_add_X_smul, Semiring.smulCommClass, Polynomial.leadingCoeff_det_X_one_add_C, mul_smul, submatrix_smul, LinearMap.toMatrixOrthonormal_reindex, matPolyEquiv_map_smul, SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, conjTranspose_natCast_smul, Represents.smul, smul_one_eq_diagonal, isScalarTower, Nondegenerate.smul_iff, derivative_det_one_add_X_smul, conjTranspose_inv_intCast_smul, det_updateRow_smul_left, op_smul_one_eq_diagonal, inv_denom_smul_num, LinearMap.toMatrixOrthonormal_apply_apply, det_smul, LieAlgebra.Orthogonal.jb_transform, det_one_add_smul, inv_smul', linftyOpIsBoundedSMul, det_smul_of_tower, MatrixEquivTensor.toFunBilinear_apply, diagonal_smul, isBoundedSMul, smul_of, conjTranspose_inv_natCast_smul, IsSymm.smul, toEuclideanCLM_toLp, adjugate_adjugate, inv_smul, smul_kroneckerTMul, inv_def, vec_smul, conjTranspose_inv_ofNat_smul, IsDiag.smul, op_smul_eq_mul_diagonal, smul_apply, LinearMap.toMatrixOrthonormal_symm_apply, Polynomial.coeff_det_X_add_C_card, instContinuousConstSMulMatrix, mul_mul_right, convex_colStochastic, inv_adjugate, det_one_add_X_smul, IsHermitian.cfcAux_apply, conjTranspose_ratCast_smul, ofLp_toEuclideanCLM, kroneckerTMulStarAlgEquiv_apply, instStarModule, Module.instIsScalarTowerForall, smul_eq_mul_diagonal, adjugate_smul, CStarMatrix.smul_of, nonsing_inv_apply, map_op_smul', adjugate_adjugate', smulCommClass, coe_toEuclideanCLM_eq_toEuclideanLin, LinearMap.toMatrixOrthonormal_apply, MatrixEquivTensor.invFun_smul, linftyOpNormSMulClass, blockDiagonal_smul, blockDiag'_smul, matrixEquivTensor_apply_symm, IsHermitian.spectral_theorem, smul_kronecker, kronecker_ofNat, detp_smul_adjp, kroneckerMap_smul_left, scalar_comm_iff, mem_skewAdjointMatricesLieSubalgebra_unit_smul, CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv, diagonal_kronecker, det_smul_adjugate_adjugate, MatrixModCat.isScalarTower_toModuleCat, instIsScalarTowerForall, extremePoints_doublyStochastic, LieAlgebra.Orthogonal.jd_transform, smul_mul, replicateCol_smul, detp_smul_add_adjp, normSMulClass, isDiag_smul_one, isAddUnit_detp_smul_mul_adjp, coeff_det_one_add_X_smul_one, conjTranspose_intCast_smul, kroneckerTMul_smul, Polynomial.natDegree_det_X_add_C_le, kroneckerMap_smul_right, transpose_smul, smul_hadamard, Semiring.isScalarTower, convex_rowStochastic, conjTranspose_ofNat_smul, frobeniusNormSMulClass, map_smul', Algebra.Norm.Transitivity.mul_auxMat_toSquareBlock_eq, IsSMulRegular.matrix, trace_smul, convex_doublyStochastic, conjTranspose_smul_non_comm, map_smulₛₗ, ofNat_kronecker, instIsScalarTowerMulOppositeForallOfSMulCommClass, det_sum_smul_le, IsHermitian.star_mul_self_mul_eq_diagonal, vecMulVec_smul, cramer_smul, conjTranspose_rat_smul, fromBlocks_smul, Algebra.Norm.Transitivity.auxMat_toSquareBlock_ne, blockDiag_smul, map_smul, conjTranspose_smul, IsLeftRegular.matrix, smul_single, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, PosSemidef.smul, cstar_norm_def, invOf_eq, conjTranspose_smul_self, det_updateCol_smul_left, IsHermitian.conjStarAlgAut_star_eigenvectorUnitary, matPolyEquiv_smul_one, replicateRow_smul, MatrixEquivTensor.toFunAlgHom_apply, vecMul_smul, scalar_commute_iff, PosDef.smul, smul_eq_diagonal_mul, adjugate_mul, derivative_det_one_add_X_smul_aux, kroneckerStarAlgEquiv_apply, mul_adjp_add_detp, exists_eq_sum_perm_of_mem_doublyStochastic, kronecker_smul, smul_mulVec, kronecker_diagonal, permanent_smul, instContinuousSMulMatrix, kroneckerStarAlgEquiv_symm_apply, QuadraticMap.toMatrix'_smul, exists_mem_doublyStochastic_eq_smul_iff, blockDiagonal'_smul, Polynomial.coeff_det_X_add_C_zero, LieAlgebra.Orthogonal.pd_inv, mul_adjugate
|
sub 📖 | CompOp | 64 mathmath: invOf_fromBlocks₂₂_eq, add_mul_mul_invOf_mul_eq_one, le_iff, IsHermitian.fromBlocks₂₂, submatrix_sub, RootPairing.Base.cartanMatrix_map_abs, BlockTriangular.sub_iff_right, fromBlocks_eq_of_invertible₁₁, PosDef.fromBlocks₁₁, sub_mul, circulant_sub, conjTranspose_sub, add_mul_mul_inv_eq_sub', add_mul_mul_inv_eq_sub, IsParabolic.sub_eigenvalue_sq_eq_zero, charpoly_sub_scalar, inv_sub_inv, sub_apply, vec_sub, map_sub, CStarMatrix.of_sub_of, schur_complement_eq₂₂, transpose_sub, det_one_sub_mul_comm, add_mul_mul_invOf_mul_eq_one', LieAlgebra.SpecialLinear.sl_bracket, det_fromBlocks₁₁, add_mul_mul_mul_invOf_eq_one, det_fromBlocks_one₁₁, isUnit_fromBlocks_iff_of_invertible₂₂, mul_sub, fromBlocks_eq_of_invertible₂₂, sub_scalar_sq_eq_disc, schur_complement_eq₁₁, invOf_add_mul_mul, det_fromBlocks_one₂₂, isUnit_fromBlocks_iff_of_invertible₁₁, blockDiagonal_sub, PosDef.fromBlocks₂₂, add_mul_mul_mul_invOf_eq_one', diagonal_sub, eval_charpoly, det_fromBlocks₂₂, BlockTriangular.sub_iff_left, sub_mulVec, vecMul_sub, blockDiag'_sub, IsHermitian.fromBlocks₁₁, invOf_add_mul_mul', blockDiag_sub, blockDiagonal'_sub, trace_sub, sub_vecMulVec, of_sub_of, IsSymm.sub, IsHermitian.sub, BlockTriangular.sub, LieAlgebra.SpecialLinear.val_singleSubSingle, PEquiv.toMatrix_swap, sub_scalar_sq_eq_discr, invOf_fromBlocks₁₁_eq, IsDiag.sub, vecMulVec_sub, diag_sub
|
subDown 📖 | CompOp | — |
subDownLeft 📖 | CompOp | — |
subDownRight 📖 | CompOp | — |
subLeft 📖 | CompOp | — |
subRight 📖 | CompOp | — |
subUp 📖 | CompOp | — |
subUpLeft 📖 | CompOp | — |
subUpRight 📖 | CompOp | — |
submatrix 📖 | CompOp | 104 mathmath: isTotallyUnimodular_iff, submatrix_diagonal, lift_cRank_submatrix_le, det_permute, abs_det_submatrix_equiv_equiv, submatrix_cons_row, submatrix_sub, submatrix_vecMul_equiv, transpose_submatrix, submatrix_smul, kroneckerTMul_assoc', det_succ_row, permanent_permute_rows, adjugate_fin_succ_eq_det_submatrix, lift_cRank_submatrix, isTotallyUnimodular_iff_fintype, eRank_submatrix, submatrix_single_equiv, fromBlocks_submatrix_sum_swap_left, submatrix_add, updateRow_submatrix_equiv, TensorProduct.toMatrix_assoc, PEquiv.toMatrix_toPEquiv_eq, fromBlocks_submatrix_sum_swap_sum_swap, submatrix_empty, submatrix_id_mul_right, reindex_apply, submatrix_updateRow_succAbove, det_eq_sum_column_mul_submatrix_succAbove_succAbove_det, isUnit_submatrix_equiv, submatrix_updateCol_equiv, submatrix_mulVec_equiv, col_submatrix, fromBlocks_submatrix_sum_swap_right, PEquiv.toMatrix_toPEquiv_mul, permanent_permute_cols, conjTranspose_submatrix, IsDiag.submatrix, rank_submatrix, one_submatrix_mul, submatrix_updateRow_equiv, submatrix_id_mul_left, BlockTriangular.submatrix, det_succ_column, diag_submatrix, isHermitian_submatrix_equiv, submatrix_one, blockDiagonal'_submatrix_eq_blockDiagonal, cRank_submatrix, kronecker_assoc', submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det', submatrix_diagonal_equiv, cramer_submatrix_equiv, mulVecLin_submatrix, det_succ_column_zero, submatrix_one_equiv, mul_submatrix_one, submatrix_one_embedding, updateCol_submatrix_equiv, adjugate_submatrix_equiv_self, det_eq_sum_row_mul_submatrix_succAbove_succAbove_det, trace_submatrix_succ, submatrix_id_id, submatrixEquivInvertibleEquivInvertible_apply, det_permute', IsSymm.submatrix, col_submatrix_eq_comp, submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det, submatrix_diagonal_embedding, inv_submatrix_equiv, toLin'_submatrix, submatrix_submatrix, Module.Basis.toMatrix_reindex, PosSemidef.submatrix, invOf_submatrix_equiv_eq, submatrix_mul_transpose_submatrix, submatrix_gram, cRank_submatrix_le, row_submatrix_eq_comp, IsHermitian.submatrix, submatrix_apply, updateCol_subsingleton, det_submatrix_equiv_self, submatrix_mul_equiv, projVandermonde_comp, updateRow_subsingleton, submatrix_map, rank_submatrix_le, submatrixEquivInvertibleEquivInvertible_symm_apply, PEquiv.mul_toMatrix_toPEquiv, submatrix_zero, det_succ_row_zero, conjTranspose_kronecker', submatrix_mul, IsTotallyUnimodular.submatrix, posSemidef_submatrix_equiv, TensorProduct.toMatrix_comm, eRank_submatrix_le, Continuous.matrix_submatrix, submatrix_mem_matrix, submatrix_updateCol_succAbove, submatrix_neg, submatrix_mem_matrix_iff, row_submatrix
|
transpose 📖 | CompOp | 247 mathmath: mulVec_transpose, SymplecticGroup.transpose_mem_iff, transposeInvertibleEquivInvertible_symm_apply, rank_transpose, PEquiv.toMatrix_symm, cramer_transpose_row_self, replicateRow_mulVec, transpose_permMatrix, LieAlgebra.Orthogonal.mem_so, toLinearMap₂'_comp, transpose_ofNat, SymplecticGroup.coe_inv, SymplecticGroup.transpose_mem, blockDiagonal_transpose, isNilpotent_transpose_iff, summable_matrix_transpose, transpose_circulant, transpose_eq_intCast, det_transpose, PosSemidef.transpose, transpose_submatrix, num_transpose, trace_transpose, QuadraticMap.toMatrix'_comp, sum_hadamard_eq, RingEquiv.mopMatrix_symm_apply, col_transpose, transpose_transpose, RingEquiv.mopMatrix_apply, LDL.lowerInv_eq_gramSchmidtBasis, transpose_eq_one, conjTranspose_eq_transpose_of_trivial, IsIrreducible.transpose, LinearMap.toMatrix₂'_compl₁₂, LDL.lowerInv_orthogonal, Algebra.traceMatrix_of_matrix_vecMul, LieAlgebra.Orthogonal.jb_transform, SymplecticGroup.mem_iff, transpose_add, transpose_replicateCol, LinearMap.toMatrix_transpose, transpose_zero, transposeRingEquiv_symm_apply, updateRow_transpose, IsHermitian.transpose, LinearMap.BilinForm.mul_toMatrix'_mul, vec_dotProduct_vec, BilinForm.mul_toMatrix_mul, toLinearMap₂_compl₁₂, isIrreducible_transpose_iff, transpose_eq_ofNat, transpose_eq_diagonal, vec_transpose, comp_transpose, AlgEquiv.mopMatrix_apply, CartanMatrix.C_transpose, Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans, mulVec_vecMul, LinearMap.toMatrix₂_comp, transpose_empty_cols, blockDiag_transpose, den_transpose, isAdjointPair_equiv', BilinForm.toMatrix_comp, transpose_list_sum, J_transpose, transpose_mul, CartanMatrix.E₆_transpose, Fin.transpose_circulant, transpose_conjTranspose, row_transpose, Algebra.embeddingsMatrixReindex_eq_vandermonde, ker_mulVecLin_transpose_mul_self, vandermonde_transpose_mul_vandermonde, transpose_multiset_sum, LinearMap.BilinForm.toMatrix'_compLeft, isSymm_add_transpose_self, transpose_sub, diag_transpose, transpose_natCast, transpose_neg, AffineBasis.det_smul_coords_eq_cramer_coords, rank_transpose_mul_self, cons_transpose, LinearMap.toMatrix_transpose_apply, transpose_map, transposeRingEquiv_apply, SimpleGraph.incMatrix_mul_transpose, transpose_isTotallyUnimodular_iff, isSymm_mul_transpose_self, col_def, LinearMap.mul_toMatrix', mul_adjugate_apply, PosDef.transpose_iff, exp_transpose, LinearMap.mul_toMatrix₂, fromBlocks_transpose, isUnit_det_transpose, transpose_zpow, transpose_invOf, norm_transpose, vandermonde_mul_vandermonde_transpose, LinearMap.toMatrix₂_compl₁₂, LinearMap.toMatrix_transpose_apply', transpose_mem_rowStochastic_iff_mem_colStochastic, IsSymm.transpose, col_eq_transpose, BilinForm.toMatrix_mul_basis_toMatrix, LinearMap.BilinForm.mul_toMatrix', CartanMatrix.D_transpose, isAdjointPair_equiv, mulVecLin_transpose, transpose_injective, transpose_vecMulVec, vec_vecMul_kronecker_of_commute, nnnorm_transpose, SymplecticGroup.mem_iff', SymplecticGroup.inv_left_mul_aux, adjugate_def, BlockTriangular.transpose, IsDiag.transpose, mulVec_eq_sum, transposeAddEquiv_apply, transpose_intCast, blockDiagonal'_transpose, transpose_fromRows, blockTriangular_transpose_iff, NumberField.inverse_basisMatrix_mulVec_eq_repr, transpose_inj, Module.Basis.coePiBasisFun.toMatrix_eq_transpose, isSimplyLaced_transpose, toBilin'_comp, posSemidef_transpose_iff, LinearMap.mul_toMatrix₂_mul, transpose_tsum, diagonal_transpose, transpose_single, LinearMap.BilinForm.mul_toMatrix_mul, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix, LinearMap.BilinForm.toMatrix'_comp, transpose_one, vec_vecMul_kronecker, mem_orthogonalGroup_iff, transpose_pow, SimpleGraph.incMatrix_mul_transpose_diag, transpose_mem_matrix_iff, SpecialLinearGroup.coe_transpose, dotProduct_vecMul_hadamard, LieAlgebra.Orthogonal.jd_transform, LinearMap.BilinForm.toMatrix_compLeft, LinearMap.BilinForm.mul_toMatrix, Summable.matrix_transpose, LinearMap.mul_toMatrix₂'_mul, IsSymm.eq, kronecker_mulVec_vec, PiLp.basis_toMatrix_basisFun_mul, tail_transpose, LinearMap.toMatrix₂_mul_basis_toMatrix, lie_transpose, SimpleGraph.incMatrix_transpose_mul_diag, mul_transpose_self_isDiag_iff_hasOrthogonalRows, trace_transpose_mul, transpose_smul, transpose_swap, PosDef.transpose, of_col, transposeAlgEquiv_apply, kroneckerMap_transpose, CartanMatrix.B_transpose, vecMulLinear_transpose, transpose_nonsing_inv, isSymm_transpose_add_self, isSymm_fromBlocks_iff, Algebra.traceMatrix_of_matrix_mulVec, CartanMatrix.E₇_transpose, toLin_transpose, BilinForm.mul_toMatrix, submatrix_mul_transpose_submatrix, Continuous.matrix_transpose, transpose_hasOrthogonalCols_iff_hasOrthogonalRows, transposeᵣ_eq, AlgEquiv.mopMatrix_symm_apply, comp_symm_transpose, transpose_eq_zero, charpoly_transpose, adjugate_transpose, transpose_fromCols, conjTranspose_transpose, HasOrthogonalRows.transpose_hasOrthogonalCols, transpose_hasOrthogonalRows_iff_hasOrthogonalCols, IsHermitian.eigenvectorUnitary_transpose_apply, Module.Basis.toMatrix_transpose_apply, PEquiv.transpose_toMatrix_toPEquiv_apply, mem_orthogonalGroup_iff', HasOrthogonalCols.transpose_hasOrthogonalRows, transpose_mul_self_isDiag_iff_hasOrthogonalCols, transpose_mem_doublyStochastic_iff, replicateCol_vecMul, BilinForm.toMatrix_compLeft, isUnit_transpose, LinearMap.toMatrix₂'_comp, LinearMap.BilinForm.toMatrix_comp, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, transpose_replicateRow, updateCol_transpose, LieAlgebra.Orthogonal.indefiniteDiagonal_transform, transpose_mem_colStochastic_iff_mem_rowStochastic, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, vecMul_transpose, transpose_empty_rows, skewAdjointMatricesLieSubalgebraEquiv_apply, transpose_apply, SimpleGraph.transpose_adjMatrix, blockDiag'_transpose, cramer_transpose_apply, comp_map_transpose, vecMul_mulVec, HasSum.matrix_transpose, permanent_transpose, CartanMatrix.A_transpose, frobenius_nnnorm_transpose, head_transpose, kronecker_mulVec_vec_of_commute, charmatrix_transpose, transpose_reindex, CartanMatrix.E₈_transpose, mulVec_one, isSymm_transpose_mul_self, LinearMap.toMatrixAlgEquiv_transpose_apply, isHermitian_transpose_iff, transposeInvertibleEquivInvertible_apply, transpose_eq_natCast, SymplecticGroup.inv_eq_symplectic_inv, transpose_list_prod, transpose_sum, LinearMap.toMatrixAlgEquiv_transpose_apply', frobenius_norm_transpose, toBilin_comp, isDiag_transpose_iff, inner_matrix_col_col, LieAlgebra.Orthogonal.pd_inv, mul_mul_apply, det_smul_inv_vecMul_eq_cramer_transpose, Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans, SimpleGraph.incMatrix_mul_transpose_apply_of_adj, IsTotallyUnimodular.transpose, rank_self_mul_transpose
|
unique 📖 | CompOp | — |
zero 📖 | CompOp | 166 mathmath: single_eq_updateRow_zero, toBlock_one_disjoint, replicateCol_zero, comp_diagonal_diagonal, RootPairing.GeckConstruction.h_def, frobeniusIsBoundedSMul, toBlock_diagonal_disjoint, PEquiv.single_mul_single_of_ne, trace_mul_conjTranspose_self_eq_zero_iff, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, zero_mulVec, isParabolic_iff_exists, hadamard_one_eq_zero_iff, isNilpotent_transpose_iff, replicateRow_zero, IsDiag.fromBlocks, kroneckerTMul_zero, inv_fromBlocks_zero₁₂_of_isUnit_iff, PosSemidef.sqrt_eq_zero_iff, zero_apply, map_zero, fromBlocks_eq_of_invertible₁₁, zero_kronecker, fromRows_zero, isNilpotent_iff_forall_row, comp_single_single, single_zero, diag_zero, LieAlgebra.Orthogonal.jb_transform, upper_two_blockTriangular, diagonal_zero, LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, inv_zero, transpose_zero, IsParabolic.sub_eigenvalue_sq_eq_zero, PEquiv.toMatrix_bot, PosSemidef.trace_eq_zero_iff, gram_zero, isNilpotent_toLin'_iff, conjTranspose_zero, linftyOpIsBoundedSMul, isBoundedSMul, isUnit_fromBlocks_zero₂₁, charpoly_zero, isSymm_zero, num_zero, mulVecLin_zero, charpoly_fromBlocks_zero₂₁, toBlocks₁₂_diagonal, den_zero, det_zero, LinearMap.isNilpotent_toMatrix_iff, blockDiag'_zero, Represents.zero, transpose_list_sum, blockTriangular_zero, of_zero, mulRightLinearMap_zero_eq_zero, blockDiag_zero, cramer_zero, PosSemidef.nonneg, nonneg_iff_posSemidef, toMvPolynomial_zero, mul_zero, mul_single_eq_updateCol_zero, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', TransvectionStruct.mul_sumInl_toMatrix_prod, eRank_zero, isStrictlyPositive_iff_posDef, mulRightLinearMap_eq_zero_iff, conjTranspose_list_sum, invOf_fromBlocks_zero₁₂_eq, single_hadamard_single_of_ne, rank_zero, empty_mul_empty, replicateRow_eq_zero, LieAlgebra.Orthogonal.s_as_blocks, trace_conjTranspose_mul_self_eq_zero_iff, circulant_zero, zero_hadamard, fromBlocks_diagonal, vec_eq_zero_iff, PosSemidef.zero, fromBlocks_eq_of_invertible₂₂, hadamard_zero, isUnit_fromBlocks_zero₁₂, blockDiagonal'_zero, LinearMap.toMatrix_prodMap, vec_zero, fromBlocks_one, comp_symm_diagonal, single_mul_single_of_ne, one_hadamard_eq_zero_iff, trace_list_sum, PosDef.isStrictlyPositive, single_mul_eq_updateRow_zero, nonsing_inv_cancel_or_zero, blockDiagonal_zero, nonsing_inv_apply_not_isUnit, toBlock_inverse_eq_zero, vecMulVec_zero, RootPairing.GeckConstruction.isNilpotent_f, charpoly_fromBlocks_zero₁₂, RootPairing.GeckConstruction.isNilpotent_e, adjugate_zero, det_fromBlocks_zero₁₂, isAdjMatrix_iff_hadamard, updateCol_zero_zero, inv_fromBlocks_zero₂₁_of_isUnit_iff, cRank_zero, vecMulVec_eq_zero, conjTranspose_eq_zero, det_fromBlocks_zero₂₁, isNilpotent_iff, zero_mul, updateRow_zero_mul_updateCol_zero, replicateCol_eq_zero, self_mul_conjTranspose_mul_eq_zero, invOf_fromBlocks_zero₂₁_eq, isHermitian_zero, zero_zpow_eq, mulLeftLinearMap_zero_eq_zero, transpose_eq_zero, kroneckerMap_zero_left, MatrixEquivTensor.invFun_zero, single_eq_updateCol_zero, kroneckerMap_zero_right, diag_list_sum, zero_vecMulVec, TransvectionStruct.sumInl_toMatrix_prod_mul, conjTranspose_mul_self_eq_zero, permanent_zero, isDiag_fromBlocks_iff, comp_diagonal, trace_zero, IsHermitian.eigenvalues_eq_zero_iff, aeval_self_charpoly, mulLeftLinearMap_eq_zero_iff, num_eq_zero_iff, fromBlocks_zero, adjugate_fin_zero, LieAlgebra.Orthogonal.pb_inv, RootPairing.GeckConstruction.lie_h_h, CStarMatrix.of_zero, TransvectionStruct.toMatrix_sumInl, conjTranspose_mul_self_mul_eq_zero, submatrix_zero, zero_zpow, comp_symm_single, self_mul_conjTranspose_eq_zero, diagonal_zero', isDiag_zero, updateRow_zero_zero, vecMul_zero, fromCols_zero, toBlocks₂₁_diagonal, isNilpotent_iff_forall_col, RootPairing.GeckConstruction.lie_e_f_ne, fromBlocks_diagonal_pow, mul_self_mul_conjTranspose_eq_zero, charmatrix_zero, kronecker_zero, zero_kroneckerTMul, LieAlgebra.SpecialLinear.sl_non_abelian, mul_conjTranspose_mul_self_eq_zero, comp_one
|
«term_ᵀ» 📖 | CompOp | — |