Matrix

📁 Source: Mathlib/Topology/UniformSpace/Matrix.lean

Statistics

Metric	Count
Definitions Matrix, instUniformSpace	2
Theorems instCompleteSpace, instIsUniformAddGroup, instT0Space, uniformContinuous, uniformity	5
Total	7

Matrix

Definitions

Name	Category	Theorems
instUniformSpace 📖	CompOp	6 math math: instCompleteSpace, instT0Space, instIsUniformAddGroup, uniformContinuous, CStarMatrix.uniformEmbedding_ofMatrix, uniformity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompleteSpace 📖	mathematical	—	CompleteSpace Matrix instUniformSpace	—	Pi.complete
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup Matrix instUniformSpace addGroup	—	Pi.instIsUniformAddGroup
instT0Space 📖	mathematical	—	T0Space Matrix UniformSpace.toTopologicalSpace instUniformSpace	—	Pi.instT0Space
uniformContinuous 📖	mathematical	—	UniformContinuous Matrix instUniformSpace	—	uniformity
uniformity 📖	mathematical	—	uniformity Matrix instUniformSpace iInf Filter Filter.instInfSet Filter.comap	—	Pi.uniformity Filter.comap_iInf Filter.comap_comap

(root)

Definitions

Name	Category	Theorems
Matrix 📖	CompOp	2533 math math: Matrix.l2_opNorm_toEuclideanCLM, Matrix.frobenius_norm_replicateCol, Matrix.single_eq_updateRow_zero, Matrix.UnitaryGroup.toLin'_one, Matrix.posSemidef_conjTranspose_mul_self, Matrix.toBlock_one_disjoint, Matrix.replicateCol_zero, Matrix.IsDiag.add, LinearMap.restrictScalars_toMatrix, Matrix.comp_diagonal_diagonal, Matrix.discr_conj, AddMonoidHom.mapMatrix_comp, Matrix.natCast_kronecker, LinearMap.SeparatingRight.toMatrix₂', Matrix.toLinAlgEquiv_one, RingHom.mapMatrix_id, Matrix.GeneralLinearGroup.det_scalar, LinearMap.charpoly_def, RootPairing.GeckConstruction.h_def, Matrix.instFinite, Matrix.vecMulVec_empty, Matrix.replicateCol_cons, Matrix.list_prod_inv_reverse, Matrix.circulant_neg, Matrix.frobenius_nnnorm_mul, ModularGroup.SLOnGLPos_smul_apply, Matrix.swap_mul_self, SymplecticGroup.transpose_mem_iff, Algebra.IsCentral.matrix, ModularForm.smul_slash, Matrix.toLin_kronecker, Matrix.toLin'_symm, Matrix.circulant_smul, Matrix.invOf_fromBlocks₂₂_eq, Matrix.SeparatingLeft.toBilin', LinearMap.detAux_def'', Matrix.transposeInvertibleEquivInvertible_symm_apply, Matrix.replicateCol_injective, LinearMap.toMatrixAlgEquiv'_mul, Matrix.GLPos.coe_neg_apply, Matrix.kroneckerTMulStarAlgEquiv_symm_apply, Matrix.frobeniusIsBoundedSMul, LinearMap.BilinForm.toMatrix_toBilin, Matrix.IsSymm.exp, Module.Basis.end_repr_apply, Matrix.linfty_opNorm_diagonal, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, Subgroup.adjoinNegOne_eq_self_iff, Matrix.star_eq_conjTranspose, Matrix.SeparatingRight.toLinearMap₂, Matrix.entryAddHom_apply, Matrix.IsHermitian.isClosedEmbedding_cfcAux, Matrix.smul_vecMulVec, Matrix.SpecialLinearGroup.map_mapGL, RootPairing.GeckConstruction.isSl2Triple, Matrix.norm_diagonal, BilinForm.toMatrix_symm, Matrix.scalar_inj, Matrix.isHermitian_conjTranspose_mul_mul, SimpleGraph.lapMatrix_toLinearMap₂', Matrix.reindexLinearEquiv_trans, Matrix.inv_mul_eq_iff_eq_mul_of_invertible, Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col, Matrix.add_mul_mul_invOf_mul_eq_one, reindex_mem_doublyStochastic_iff, Matrix.GeneralLinearGroup.map_det, Matrix.isCentralScalar, Matrix.GeneralLinearGroup.val_mkOfDetNeZero, Matrix.abs_det_reindex, Algebra.Norm.Transitivity.polyToMatrix_cornerAddX, Matrix.scalar_comm, Matrix.separatingRight_toLinearMap₂'_iff, ZSpan.volume_real_fundamentalDomain, Matrix.toBlock_diagonal_disjoint, Matrix.hadamard_smul, Matrix.kronecker_natCast, Matrix.diagonal_natCast, Matrix.det_smul_inv_mulVec_eq_cramer, Matrix.SpecialLinearGroup.continuous_toGL, Matrix.pow_eq_aeval_mod_charpoly, Matrix.diagonal_mem_matrix_iff, Matrix.IsHermitian.zpow, Matrix.UnitaryGroup.toGL_mul, Subgroup.instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL, Matrix.Commute.zpow_self, Polynomial.toMatrix_sylvesterMap', Matrix.IsHermitian.det_abs, Matrix.posSemidef_iff_eq_conjTranspose_mul_self, Matrix.toLinearMapRight'_mul, ModularForm.mul_slash, Matrix.one_div_pow, Matrix.det_add_replicateCol_mul_replicateRow, Matrix.GeneralLinearGroup.IsParabolic.parabolicFixedPoint_pow, PEquiv.single_mul_single_of_ne, LinearMap.mapMatrix_zero, Matrix.separatingRight_toLinearMap₂_iff, Matrix.isUnit_det_zpow_iff, Matrix.SpecialLinearGroup.coeToGL_det, AddMonoidHom.mapMatrix_id, Matrix.replicateRow_mulVec, RootPairing.GeckConstruction.instHasTrivialRadical, Matrix.trace_mul_conjTranspose_self_eq_zero_iff, Matrix.compAlgEquiv_apply, Matrix.spectrum_toEuclideanLin, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, ModuleCat.toMatrixModCat_map, Matrix.cstar_nnnorm_def, LieAlgebra.Orthogonal.mem_so, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, Matrix.IsHermitian.cfc_eq, LinearMap.mapMatrixLinear_apply, IsMoritaEquivalent.matrix, Matrix.GeneralLinearGroup.map_comp_apply, LinearMap.BilinForm.toMatrixAux_eq, Matrix.mul_mul_left, Matrix.det_det, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, Matrix.toLinearMap₂'_comp, Matrix.adjugate_fin_two, Matrix.l2_opNorm_mulVec, Matrix.diagonal_vec3, Matrix.transpose_ofNat, kroneckerTMulAlgEquiv_symm_single_tmul, SymplecticGroup.coe_inv, UpperHalfPlane.re_smul, Matrix.zero_mulVec, Matrix.Pivot.length_listTransvecRow, LinearMap.toMatrix_apply', Matrix.isHermitian_conjTranspose_mul_self, mem_pairSelfAdjointMatricesSubmodule, Matrix.one_kronecker, LinearMap.toMatrix₂_mul, Matrix.conjTranspose_sum, Matrix.vec_add, Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL, Matrix.lieConj_apply, Matrix.natCast_apply, Matrix.norm_def, LinearMap.entryLinearMap_comp_mapMatrix, Matrix.repr_toLin, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, Matrix.mul_single_apply_same, Matrix.SpecialLinearGroup.toGLPos_injective, CartanMatrix.C_two, LinearMap.toMatrixAlgEquiv_comp, Matrix.isParabolic_iff_exists, SymplecticGroup.coe_J, Matrix.diag_smul, Algebra.norm_eq_matrix_det, Matrix.le_iff, LinearEquiv.mapMatrix_apply, Matrix.liftLinear_single, Polynomial.sylvester_comm, Matrix.IsHermitian.fromBlocks₂₂, ZMod.charpoly_pow_card, eval_det_add_X_smul, Matrix.Pivot.listTransvecCol_mul_last_col, Matrix.reindex_mem_colStochastic_iff, instContinuousStarMatrix, Matrix.hadamard_one_eq_zero_iff, Matrix.entryAddHom_eq_comp, Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, LinearMap.BilinForm.toMatrix_compRight, Matrix.mul_apply', Matrix.mul_inv_eq_iff_eq_mul_of_invertible, CongruenceSubgroup.exists_Gamma_le_conj', Matrix.transposeLinearEquiv_symm, Matrix.specialUnitaryGroup_le_unitaryGroup, Matrix.posSemidef_self_mul_conjTranspose, Matrix.Semiring.smulCommClass, Matrix.diagonal_fin_two, Matrix.submatrix_sub, Matrix.trace_units_conj, Matrix.mul_invOf_eq_iff_eq_mul_right, Matrix.vec_sum, Matrix.add_mulVec, RootPairing.Base.cartanMatrix_map_abs, Polynomial.leadingCoeff_det_X_one_add_C, Matrix.toLinearMap₂_toMatrix₂, LinearMap.toMatrix_one, ModularGroup.bottom_row_coprime, Matrix.zpow_neg_one, Matrix.isNilpotent_transpose_iff, summable_matrix_transpose, Matrix.toSquareBlock_def, SlashInvariantForm.quotientFunc_mk, Matrix.mul_smul, ModularForm.SL_slash, CongruenceSubgroup.conjGL_coe, Matrix.separatingRight_toBilin_iff, TwoSidedIdeal.equivMatrix_symm_apply_ringCon, Matrix.conjTranspose_mul_self_mulVec_eq_zero, Matrix.spectrum_toLpLin, Matrix.kronecker_add, Matrix.single_add, Matrix.replicateRow_zero, ModuleCat.matrixEquivalence_inverse, Matrix.diagonal_natCast', Matrix.IsDiag.fromBlocks, UpperHalfPlane.im_smul_eq_div_normSq, Matrix.kroneckerTMul_zero, Matrix.sum_single_one, Matrix.transpose_eq_intCast, Matrix.charmatrix_reindex, NumberField.Units.regOfFamily_eq_det, Matrix.vec_neg, Matrix.isHyperbolic_conj_iff, CartanMatrix.D_four, LinearMap.BilinForm.toMatrix'_symm, UpperHalfPlane.specialLinearGroup_apply, Matrix.detp_neg_one_one, Matrix.toLin_mul_apply, toMatrix_distrib_mul_action_toLinearMap, RingHom.mapMatrix_apply, Matrix.GeneralLinearGroup.map_inv_mul_map, Matrix.mulVec_injective, Matrix.toMvPolynomial_add, mem_doublyStochastic_iff_sum, Matrix.linfty_opNorm_replicateRow, LieModule.instIsFaithfulMatrixForall, Matrix.PosSemidef.intCast, Matrix.charpoly_units_conj', Matrix.transposeAddEquiv_symm, LinearMap.BilinForm.toMatrix'_apply, TwoSidedIdeal.matrix_jacobson_bot, RingCon.matrix_strictMono_of_nonempty, ModuleCat.toMatrixModCat_obj_carrier, Matrix.PosSemidef.sqrt_eq_zero_iff, LinearMap.BilinForm.SeparatingRight.toMatrix, Matrix.submatrix_smul, Matrix.kroneckerMap_reindex_right, LinearMap.nondegenerate_toLinearMap₂'_of_det_ne_zero', Matrix.SpecialLinearGroup.scalar_eq_self_of_mem_center, Matrix.frobenius_nnnorm_map_eq, Matrix.blockDiagonal'RingHom_apply, Matrix.Nondegenerate.toLinearMap₂, Matrix.nonempty, Matrix.permMatrix_mem_rowStochastic, Matrix.blockDiagonal_tsum, UpperHalfPlane.num_neg, Matrix.mul_right_injective_of_invertible, Matrix.intrinsicStar_toLin', RingCon.matrix_top, UpperHalfPlane.moebius_im, Set.mem_matrix, Matrix.zero_apply, ModularForm.prod_slash, AddMonoidHom.mapMatrix_zero, Matrix.mem_spectrum_iff_isRoot_charpoly, Algebra.smul_leftMulMatrix, Matrix.IsHermitian.isSelfAdjoint, Matrix.mem_range_scalar_iff_commute_transvectionStruct, Matrix.vecMul_neg, LinearMap.toMatrixOrthonormal_reindex, LinearMap.toMatrixAlgEquiv_toLinAlgEquiv, Matrix.BlockTriangular.sub_iff_right, QuadraticMap.toMatrix'_comp, Matrix.sum_hadamard_eq, Matrix.mul_val_succ, OnePoint.smul_infty_eq_self_iff, Matrix.GeneralLinearGroup.coe_toLin, mulRightLinearMap_one, SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, Matrix.kroneckerMap_assoc₁, Matrix.map_zero, ModularGroup.bottom_row_surj, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, CongruenceSubgroup.strictPeriods_Gamma0, Algebra.map_leftMulMatrix_localization, Matrix.exists_right_inverse_iff_isUnit, Matrix.toBlock_mul_eq_add, matPolyEquiv_map_smul, Matrix.PosSemidef.commute_iff, star_dotProduct_toMatrix₂_mulVec, Matrix.zero_le_one_elem, RingEquiv.mopMatrix_symm_apply, Matrix.blockDiag_one, Module.Basis.toMatrix_smul, Matrix.exp_neg, Matrix.diagonal_vec1, ModularForm.norm_eq_zero_iff, Matrix.map_mul_natCast, Matrix.PosSemidef.natCast, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, Matrix.neg_vecMul_neg, Matrix.conjTranspose_natCast_smul, ModuleCat.toMatrixModCat_obj_isAddCommGroup, Matrix.diagonal_pow, Matrix.Represents.smul, Matrix.toMvPolynomial_one, Matrix.smul_one_eq_diagonal, Matrix.matrix_eq_sum_single, Matrix.toBilin_symm, LinearMap.spectrum_toMatrix', Real.smul_map_diagonal_volume_pi, matPolyEquiv_diagonal_X, Matrix.uniqueAddEquiv_apply, toMatrix_rotation, Matrix.GeneralLinearGroup.isParabolic_conj_iff, ZMod.trace_pow_card, AlgHom.mulLeftRightMatrix.inv_comp, Matrix.isDiag_one, Matrix.isHermitian_mul_conjTranspose_self, Matrix.diagLinearMap_apply, Matrix.diagonalLinearMap_apply, ModularForm.prod_slash_sum_weights, Matrix.IsHermitian.add, Matrix.sum_sum_single, Matrix.rank_one, Matrix.isScalarTower, Matrix.updateRow_mul, Matrix.IsSymm.pow, Matrix.fromBlocks_eq_of_invertible₁₁, Matrix.nnnorm_lt_iff, Matrix.toLpLin_mul_same, Matrix.isHyperbolic_conj'_iff, ModularGroup.coe_apply_complex, LinearMap.toMatrix_baseChange, Matrix.charpoly_natCast, spectrum_diagonal, Matrix.one_apply, CStarMatrix.ofMatrix_apply, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, Matrix.frobenius_normedStarGroup, TwoSidedIdeal.equivMatrix_apply, ModularForm.levelOne_neg_weight_rank_zero, RingHom.map_matrix_mul, RingEquiv.mopMatrix_apply, Matrix.kroneckerMap_reindex, Subgroup.IsArithmetic.is_commensurable, Subgroup.IsArithmetic.inter, Matrix.isElliptic_conj'_iff, Matrix.zero_kronecker, LinearMap.trace_eq_matrix_trace_of_finset, ModularGroup.sl_moeb, Matrix.SeparatingLeft.toLinearMap₂', Matrix.GeneralLinearGroup.center_eq_range_scalar, IsCoprime.mulVecSL, Algebra.traceMatrix_localizationLocalization, TwoSidedIdeal.matrix_top, Matrix.IsHermitian.eigenvectorUnitary_col_eq, Matrix.fromRows_zero, Matrix.rank_mul_le_right, Matrix.Nondegenerate.smul_iff, Equiv.mapMatrix_symm, LinearMap.BilinForm.nondegenerate_toMatrix_iff, Matrix.derivative_det_one_add_X_smul, Matrix.transpose_eq_one, Matrix.diagonal_one', LinearMap.toMatrixₛₗ₂'_symm, Matrix.trace_multiset_sum, Matrix.norm_entry_le_entrywise_sup_norm, Matrix.updateCol_reindex, LinearMap.rank_diagonal, Matrix.PosDef.fromBlocks₁₁, Matrix.isNilpotent_iff_forall_row, Matrix.comp_single_single, Matrix.neg_mulVec_neg, Equiv.mapMatrix_apply, rank_matrix_module, LinearMap.separatingRight_toMatrix₂'_iff, Matrix.toEuclideanLin_apply, TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r, Matrix.single_zero, Matrix.add_apply, Algebra.toMatrix_lmul_eq, Matrix.permMatrixHom_apply, Matrix.isDiag_neg_iff, Matrix.addMonoidHomMulLeft_apply, Subgroup.instHasDetOneMinGeneralLinearGroup_1, LinearMap.toMatrixAlgEquiv'_id, isAdjointPair_toLinearMap₂, Matrix.uniqueRingEquiv_apply, Matrix.diag_zero, CuspForm.coe_trace, Matrix.vandermonde_succ, Matrix.IsHermitian.neg, Matrix.sub_mul, Matrix.PosDef.posSemidef_add, Matrix.conjTranspose_inv_intCast_smul, Matrix.conjTranspose_natCast, instSMulCommClassMatrixFinOfNatNatProd, Matrix.linfty_opNNNorm_mulVec, UpperHalfPlane.J_sq, Matrix.liftLinear_singleLinearMap, Matrix.PosDef.add, Matrix.charpoly_mul_comm_of_le, Matrix.det_updateRow_smul_left, LinearEquiv.mapMatrix_toLinearMap, CongruenceSubgroup.exists_Gamma_le_conj, Matrix.liftLinear_comp_singleLinearMap, Continuous.matrix_replicateCol, Matrix.op_smul_one_eq_diagonal, LinearMap.toMatrix_symm, Matrix.toBilin_apply, Matrix.PosSemidef.conjTranspose_mul_mul_same, LinearMap.toMatrix₂'_compl₁₂, Matrix.circulant_sub, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, Matrix.det_units_conj', Module.Basis.toLin_toMatrix, Matrix.inv_denom_smul_num, Matrix.PosSemidef.sq_eq_sq_iff, Matrix.updateRow_eq_transvection, instDiscreteTopologyMatrixOfFinite, Matrix.mul_inv_of_invertible, AffineBasis.toMatrix_mul_toMatrix, LinearMap.toMatrixOrthonormal_apply_apply, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, Matrix.toLin'_mul_apply, Matrix.diag_replicateCol_mul_replicateRow, Matrix.submatrix_add, Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde, Matrix.coe_units_inv, Matrix.toLinearMapₛₗ₂'_single, UpperHalfPlane.denom_cocycle_σ, Matrix.nondegenerate_toBilin'_iff, Matrix.vec_of, Algebra.Norm.Transitivity.comp_det_mul_pow, Matrix.trace_mul_comm, Algebra.traceMatrix_of_matrix_vecMul, Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL, Matrix.det_smul, Matrix.SpecialLinearGroup.isClosedEmbedding_toGL, Matrix.minpoly_dvd_charpoly, Matrix.SpecialLinearGroup.coe_one, LinearMap.toMatrixAlgEquiv_apply, Matrix.center_eq_range, Matrix.subsingleton_of_empty_right, Matrix.det_add_mul, Matrix.conjTranspose_sub, LinearMap.toMatrix'_toLin', Subgroup.mem_adjoinNegOne_iff, Matrix.blockDiagonal'_one, LieAlgebra.Orthogonal.jb_transform, Matrix.mul_right_inj_of_invertible, Matrix.PosSemidef.one, TensorProduct.toMatrix_assoc, SymplecticGroup.mem_iff, Matrix.toLinearMap₂'_apply', Matrix.transpose_add, Matrix.ext_iff_trace_mul_right, Matrix.Pivot.mul_listTransvecRow_last_col, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, Matrix.det_one_add_smul, LinearMap.toMatrix_id, LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec, MatrixEquivTensor.invFun_add, Matrix.mul_reindexLinearEquiv_one, ModularGroup.tendsto_abs_re_smul, Matrix.add_kronecker, Matrix.ker_mulVecLin_conjTranspose_mul_self, Matrix.upper_two_blockTriangular, Matrix.toAlgEquiv_kroneckerStarAlgEquiv, SimpleGraph.mul_adjMatrix_apply, Matrix.PosSemidef.posDef_iff_isUnit, Matrix.diagonal_zero, CategoryTheory.HomOrthogonal.matrixDecomposition_id, LinearMap.toMatrix_transpose, LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, Equiv.mapMatrix_trans, LinearMap.toMatrix₂_toLinearMapₛₗ₂, Matrix.isParabolic_conj'_iff, Matrix.inv_zero, Matrix.hadamard_of_one, Matrix.mulVecLin_add, Matrix.mul_left_inj_of_invertible, Matrix.coe_ofAddEquiv_symm, Matrix.IsHermitian.eigenvectorUnitary_mulVec, Algebra.traceMatrix_reindex, Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex, Matrix.det_kroneckerMapBilinear, Matrix.diagonal_vec2, Matrix.toLinAlgEquiv_mul, Subring.coe_matrix, SlashInvariantForm.coe_translate, Matrix.transpose_zero, Matrix.SpecialLinearGroup.toLin'_symm_to_linearMap, mem_skewAdjointMatricesSubmodule', Matrix.mul_inv_cancel_right_of_invertible, Matrix.vecMulBilin_apply, Matrix.frobenius_nnnorm_one, Matrix.instCompleteSpace, Matrix.transvection_mul_transvection_same, Matrix.instSMulCommClassForall_1, Matrix.map_mul_ratCast, Matrix.sum_apply, Matrix.GeneralLinearGroup.upperRightHom_apply, Matrix.PosSemidef.det_sqrt, IsBaseChange.endHom_toMatrix, Matrix.adjugate_fin_one, Matrix.transposeRingEquiv_symm_apply, Real.map_matrix_volume_pi_eq_smul_volume_pi, Matrix.blockDiagonal'_neg, Matrix.blockDiagonal_injective, Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, Matrix.conjTranspose_tsum, Matrix.one_apply_ne, Matrix.GeneralLinearGroup.val_mk'', Matrix.PosDef.conjTranspose_mul_mul_same, Matrix.toAlgEquiv_kroneckerTMulStarAlgEquiv, PEquiv.toMatrix_toPEquiv_eq, Matrix.inv_smul', Matrix.uniqueEquiv_symm_apply, Matrix.piRingEquiv_apply, TwoSidedIdeal.matrix_bot, Matrix.toLinearMap₂'_apply, matPolyEquiv_coeff_apply_aux_1, Matrix.uniqueAddEquiv_symm_apply, LinearMap.BilinForm.separatingLeft_toMatrix'_iff, isCusp_SL2Z_iff', Matrix.linfty_opNNNorm_eq_opNNNorm, Matrix.IsParabolic.sub_eigenvalue_sq_eq_zero, ModularGroup.lcRow0Extend_symm_apply, PEquiv.toMatrix_bot, isSemisimpleRing_iff_pi_matrix_divisionRing, Algebra.leftMulMatrix_injective, Matrix.mem_unitaryGroup_iff, Matrix.one_eq_pi_single, Matrix.charpoly_sub_scalar, TwoSidedIdeal.jacobson_matrix, ModularGroup.denom_apply, Matrix.hadamard_one, Matrix.diagonal_ofNat', Matrix.PosSemidef.trace_eq_zero_iff, Module.Basis.matrix_apply, Matrix.gram_zero, Matrix.conjTransposeLinearEquiv_apply, Matrix.single_mem_matrix, Matrix.mem_spectrum_of_isRoot_charpoly, Matrix.isNilpotent_toLin'_iff, IsCoprime.vecMulSL, Matrix.star_vec_dotProduct_vec, Matrix.IsHermitian.charpoly_cfc_eq, Matrix.mul_assoc, Matrix.mul_apply_eq_vecMul, ModuleCat.matrixEquivalence_functor, LinearMap.detAux_def, Matrix.one_fromCols_isTotallyUnimodular_iff, RingCon.ofMatrix_rel, Matrix.vecMulVec_add, matPolyEquiv_symm_apply_coeff, Matrix.adjugate_fin_three, Matrix.natCast_fin_three, Matrix.toLinearEquiv'_symm_apply, LinearMap.BilinForm.mul_toMatrix'_mul, OnePoint.smul_some_eq_ite, Matrix.entryAddMonoidHom_eq_comp, Matrix.toLin_symm, Matrix.SpecialLinearGroup.det_coe, Matrix.GeneralLinearGroup.continuous_det, LinearMap.toMatrixAlgEquiv_id, Matrix.PosDef.natCast, Matrix.conjTranspose_zero, CartanMatrix.D_three, Matrix.vec_dotProduct_vec, Matrix.SpecialLinearGroup.map_apply_coe, PEquiv.mul_toMatrix_apply, Matrix.permanent_one, Matrix.coe_detMonoidHom, Matrix.neg_of, BilinForm.mul_toMatrix_mul, Matrix.isUnits_det_units, Matrix.zpow_add, Module.Basis.linearMap_apply, Matrix.zpow_add_of_nonneg, Matrix.mem_specialOrthogonalGroup_iff, Matrix.eta_fin_three, Matrix.toLinearMap₂_compl₁₂, Matrix.eRank_reindex, UpperHalfPlane.σ_mul, PowerBasis.leftMulMatrix, mem_pairSelfAdjointMatricesSubmodule', NumberField.Units.regulator_eq_det, Matrix.PosSemidef.posSemidef_sqrt, Matrix.transpose_eq_ofNat, Matrix.replicateRow_empty, Matrix.map_injective, Matrix.of_add_of, Matrix.linftyOpIsBoundedSMul, Matrix.det_smul_of_tower, Matrix.toLinearMapₛₗ₂'_symm, continuous_matrix, RootPairing.GeckConstruction.lie_h_e, summable_matrix_diagonal, AddEquiv.mapMatrix_trans, Matrix.dite_apply, Matrix.comp_transpose, MatrixEquivTensor.toFunBilinear_apply, Matrix.reindex_mem_rowStochastic_iff, Matrix.piRingEquiv_symm_apply, doublyStochastic_eq_rowStochastic_inf_colStochastic, Matrix.mulᵣ_eq, TwoSidedIdeal.mem_matrix, Matrix.permMatrix_mul, Matrix.neg_apply, LinearMap.toBilin'Aux_toMatrixAux, ModularGroup.c_eq_zero, Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec, Matrix.piLinearEquiv_apply, LinearMap.toMatrix₂_compl₂, Matrix.circulant_add, Matrix.diagonal_smul, Matrix.one_fromRows_isTotallyUnimodular_iff, mulRightLinearMap_eq_mulRight, Subgroup.commensurable_adjoinNegOne_self, Matrix.toLpLin_symm_pow, Matrix.isBoundedSMul, Matrix.smul_of, Matrix.conjTranspose_inv_natCast_smul, Matrix.replicateRow_cons, Matrix.PosDef.isUnit, Matrix.IsHermitian.exp, Matrix.TransvectionStruct.det_toMatrix_prod, Matrix.finite_spectrum, Matrix.frobenius_norm_map_eq, LinearEquiv.mapMatrix_symm, Matrix.instIsStablyFiniteRing, Matrix.toLinearMapₛₗ₂'_aux_eq, Matrix.isUnit_fromBlocks_zero₂₁, MatrixEquivTensor.invFun_algebraMap, AlgEquiv.mopMatrix_apply, Matrix.ite_apply, Matrix.eigenvalues_conjTranspose_mul_self_nonneg, Matrix.adjugate_mul_distrib_aux, Matrix.charpoly_zero, Matrix.pow_apply_nonneg, NumberField.Units.finrank_mul_regOfFamily_eq_det, Matrix.linfty_opNNNorm_toMatrix, Matrix.blockDiag_add, Ideal.single_mem_jacobson_matrix, Matrix.isRepresentation.toEnd_represents, Matrix.IsSymm.smul, Matrix.frobenius_norm_conjTranspose, Subgroup.strictWidthInfty_eq_one_of_T_mem, Matrix.toEuclideanCLM_toLp, Algebra.traceForm_toMatrix, Matrix.isUnit_nonsing_inv_det_iff, ZSpan.volume_fundamentalDomain, basis_toMatrix_basisFun_mul, Matrix.det_reindexAlgEquiv, Matrix.toLin_scalar, Matrix.submatrix_id_mul_right, Matrix.fromBlocks_mul_fromRows, Matrix.num_neg, toBilin'Aux_toMatrixAux, Matrix.detp_one_one, Matrix.reindex_apply, Matrix.PosSemidef.sqrt_eq_one_iff, Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans, BilinForm.dotProduct_toMatrix_mulVec, Matrix.adjugate_adjugate, Matrix.isSymm_zero, Matrix.PosSemidef.sqrt_sq, Matrix.num_zero, Matrix.toLpLin_one, Continuous.matrix_vecMulVec, Matrix.Fin.circulant_mul_comm, Matrix.natCast_fin_two, Matrix.star_apply, charpoly_leftMulMatrix, Subgroup.negOne_mem_adjoinNegOne, Matrix.invOf_eq_nonsing_inv, LinearMap.isPosSemidef_iff_posSemidef_toMatrix, Matrix.inv_smul, Matrix.sub_apply, Matrix.inv_reindex, Matrix.det_map, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, Matrix.subsemiringCenter_eq_scalar_map, RingCon.coe_ofMatrix_eq_relationMap, Matrix.singleLinearMap_apply, Matrix.mul_updateCol, Matrix.SpecialLinearGroup.mapGL_injective, ModularGroup.SL_to_GL_tower, Matrix.mulVec_vecMul, Matrix.eta_fin_two, Matrix.piLp_ofLp_toEuclideanLin, LinearMap.BilinForm.toMatrix_apply, ModularFormClass.one_mem_strictPeriods_SL2Z, Summable.matrix_diagonal, OnePoint.map_smul, Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm, Matrix.SpecialLinearGroup.isCoprime_col, lieEquivMatrix'_apply, Matrix.det_sum_le, BilinForm.toMatrix_toBilin, Matrix.isRegular_of_isLeftRegular_det, ModularGroup.T_mul_apply_one, Matrix.updateRow_reindex, Matrix.mulVecLin_zero, SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux, Matrix.SpecialLinearGroup.mapGL_inj, Matrix.TransvectionStruct.inv_mul, Matrix.conjTranspose_zsmul, Matrix.blockDiagonal_neg, LinearMap.minpoly_toMatrix', Matrix.GeneralLinearGroup.IsParabolic.pow, Matrix.PosSemidef.eq_sqrt_iff_sq_eq, Matrix.kroneckerMap_one_one, Matrix.exp_diagonal, Matrix.smul_kroneckerTMul, LinearMap.toMatrix₂_comp, Matrix.l2_opNNNorm_mulVec, Matrix.instFiniteSpectrum, AlgHom.map_adjugate, Matrix.charpoly.univ_coeff_eval₂Hom, Matrix.mul_neg, Matrix.TransvectionStruct.toMatrix_reindexEquiv_prod, Matrix.invOf_mul_eq_iff_eq_mul_left, Matrix.charpoly_fromBlocks_zero₂₁, AlgEquiv.mapMatrix_refl, Matrix.addMonoidHomMulRight_apply, Matrix.SeparatingRight.toLinearMap₂', Matrix.vec_sub, Matrix.BlockTriangular.neg, ModularForm.levelOne_weight_zero_rank_one, Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux, CongruenceSubgroup.strictWidthInfty_Gamma0, Matrix.one_zpow, Matrix.map_sub, Matrix.map_one, Matrix.pow_apply_pos_iff_nonempty_path, Matrix.fromBlocks_add, Matrix.J_squared, Matrix.conjTranspose_nonsing_inv, Matrix.toLpLin_pow, Matrix.transpose_empty_cols, CartanMatrix.D_three', CongruenceSubgroup.IsArithmetic.conj, Matrix.nonsing_inv_mul, Matrix.kroneckerAlgEquiv_apply, Matrix.fromRows_neg, Matrix.map_algebraMap, Matrix.toBlocks₁₂_diagonal, Matrix.toBlock_mul_eq_mul, Matrix.l2_opNorm_diagonal, LinearMap.BilinForm.separatingRight_toMatrix'_iff, Matrix.isUnit_toLin'_iff, Matrix.den_zero, Matrix.l2_opNorm_conjTranspose_mul_self, Matrix.eRank_one, UpperHalfPlane.denom_cocycle, Matrix.det_zero, Matrix.GeneralLinearGroup.coe_one, Matrix.rank_mul_eq_right_of_isUnit_det, RootPairing.GeckConstruction.trace_toEnd_eq_zero, Matrix.mul_kronecker_mul, Matrix.toLin'_mul, Matrix.of_one_hadamard, ModularGroup.lcRow0Extend_apply, LinearMap.isNilpotent_toMatrix_iff, Matrix.instLieModuleForall, LinearMap.BilinForm.dotProduct_toMatrix_mulVec, LinearMap.det_eq_det_toMatrix_of_finset, Matrix.IsTotallyUnimodular.fromCols_one, LinearMap.toMatrix_reindexRange, Matrix.norm_map_eq, Matrix.isUnit_submatrix_equiv, Matrix.mul_apply, Matrix.inv_def, Matrix.Module.smul_def, CStarMatrix.of_sub_of, Matrix.diagonal_ofNat, Matrix.GeneralLinearGroup.val_mk', Matrix.ofLp_toLpLin, Matrix.norm_le_iff, Matrix.GeneralLinearGroup.map_comp, Matrix.circulant_single_one, Matrix.blockDiag'_zero, Matrix.toMatrix₂Aux_toLinearMap₂'Aux, Matrix.toBilin'_symm, Matrix.BlockTriangular.add_iff_right, ModularGroup.coe_T_inv, Matrix.exp_nsmul, ModularGroup.T_inv_mul_apply_one, Matrix.PosDef.one, LinearMap.toMatrix_smulBasis_left, Matrix.UnitaryGroup.one_apply, AddMonoidHom.entryAddMonoidHom_comp_mapMatrix, Matrix.TransvectionStruct.toMatrix_reindexEquiv, Matrix.mulVecLin_one, FixedDetMatrices.reps_entries_le_m', Matrix.frobenius_norm_def, LinearMap.det_toLin', LinearMap.mapMatrixModule_apply, Matrix.vec_smul, Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt, Matrix.PosSemidef.mul_mul_conjTranspose_same, Matrix.Represents.zero, Matrix.kroneckerMapBilinear_apply_apply, Subgroup.IsArithmetic.isFiniteRelIndexSL, Matrix.rank_eq_finrank_range_toLin, LDL.lower_conj_diag, Matrix.toLinearMapRight'_mul_apply, AlgHom.map_det, BilinForm.toMatrix_comp, Matrix.GeneralLinearGroup.map_inv, Matrix.charmatrix_fromBlocks, Matrix.reindexLinearEquiv_one, Matrix.isParabolic_conj_iff, Matrix.transpose_list_sum, Matrix.blockTriangular_zero, Matrix.toLin_mul, Matrix.of_zero, Matrix.fromBlocks_neg, Matrix.toLin_pow, CartanMatrix.B_two, Matrix.toLin_self, kroneckerTMulLinearEquiv_one, Matrix.singleAddMonoidHom_apply, Matrix.transvection_zero, Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem, Matrix.l2_opNNNorm_conjTranspose, Matrix.J_transpose, Matrix.transvection_mul_apply_same, Matrix.transpose_mul, mulRightLinearMap_zero_eq_zero, AddMonoidHom.mapMatrix_sub, Matrix.conjTranspose_inv_ofNat_smul, LinearMap.separatingLeft_toMatrix₂'_iff, Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff, AddEquiv.entryAddHom_comp_mapMatrix, Matrix.IsDiag.smul, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, Matrix.blockDiag_zero, Matrix.mul_single_apply_of_ne, summable_matrix_conjTranspose, Matrix.comp_toSquareBlock, Matrix.cramer_zero, hasEigenvector_toLin'_diagonal, Matrix.GeneralLinearGroup.toLin'_apply, LinearMap.mapMatrixModule_id_apply, Matrix.one_hadamard_eq_diagonal_iff, LinearMap.toMatrixAlgEquiv'_apply, Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin, CongruenceSubgroup.isArithmetic_conj_SL2Z, Matrix.PosSemidef.nonneg, Matrix.fin_two_smul_prod, Matrix.IsTotallyUnimodular.one_fromRows, Matrix.reindexLinearEquiv_comp, EisensteinSeries.q_expansion_riemannZeta, Matrix.schur_complement_eq₂₂, Matrix.toLinearMapₛₗ₂'_toMatrix', LinearMap.toMatrix'_algebraMap, Matrix.cramer_reindex, Matrix.op_smul_eq_mul_diagonal, Matrix.smul_apply, PiToModule.fromMatrix_apply_single_one, Matrix.nonneg_iff_posSemidef, AlgHom.mapMatrix_apply, Matrix.isHermitian_iff_isSelfAdjoint, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, Matrix.adjugate_fin_three_of, Matrix.single_mul_apply_same, Matrix.exp_zsmul, Matrix.mem_range_scalar_iff_commute_single, Matrix.UnitaryGroup.one_val, BilinearForm.toMatrixAux_eq, ModularGroup.denom_S, Matrix.TransvectionStruct.prod_mul_reverse_inv_prod, Matrix.toMvPolynomial_zero, RootPairing.GeckConstruction.span_range_h'_eq_top, Matrix.SeparatingLeft.toBilin, Matrix.charpoly_toLin, LinearMap.toMatrixOrthonormal_symm_apply, Matrix.replicateRow_add, Matrix.SpecialLinearGroup.isCoprime_row, SimpleGraph.IsSRGWith.matrix_eq, instContinuousMulMatrixOfContinuousAdd, Polynomial.coeff_det_X_add_C_card, PEquiv.toMatrix_toPEquiv_mul, Matrix.reindex_isTotallyUnimodular, LinearMap.toMatrix_mulVec_repr, LinearMap.toMatrix_innerₛₗ_apply, Matrix.permMatrix_l2_opNorm_le, Matrix.uniqueAlgEquiv_apply, evalRingHom_mapMatrix_comp_polyToMatrix, Matrix.IsDiag.neg, Matrix.conjTransposeLinearEquiv_symm, Matrix.mul_zero, Matrix.ext_iff_trace_mul_left, Matrix.toLin_apply_eq_zero_iff, Matrix.kroneckerMap_reindex_left, Matrix.eigenvalues_self_mul_conjTranspose_nonneg, Matrix.ker_mulVecLin_transpose_mul_self, Matrix.nonsing_inv_nonsing_inv, Matrix.nondegenerate_toBilin_iff, Matrix.vandermonde_transpose_mul_vandermonde, Matrix.SpecialLinearGroup.isInducing_mapGL, instContinuousConstSMulMatrix, Matrix.BlockTriangular.add, Matrix.toLin'_reindex, Matrix.blockDiagonal'_injective, Matrix.transpose_multiset_sum, Matrix.PosSemidef.toLinearMap₂'_zero_iff, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing, LinearMap.BilinForm.toMatrix'_compLeft, Matrix.toLinearMapₛₗ₂_apply, Matrix.mul_mul_right, Matrix.convex_colStochastic, Matrix.l2_opNorm_conjTranspose, Matrix.diag_multiset_sum, Matrix.isSymm_add_transpose_self, Matrix.vecMulVec_mul, Matrix.IsSymm.zpow, continuousAt_matrix_inv, Matrix.instNonnegSpectrumClass, MatrixModCat.toModuleCat_obj_carrier, Matrix.ofNat_fin_three, Matrix.GeneralLinearGroup.continuous_upperRightHom, UpperHalfPlane.im_smul, Matrix.conjTranspose_eq_natCast, Matrix.comp_apply, Module.Basis.end_apply, Matrix.adjugate_eq_one_of_card_eq_one, Matrix.PosDef.conjTranspose_mul_self, Matrix.adjugate_reindex, Matrix.sum_single_ofNat, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, Matrix.mul_single_eq_updateCol_zero, Matrix.compRingEquiv_symm_apply, OnePoint.IsZeroAt.smul_iff, commute_mulLeftLinearMap_mulRightLinearMap, Matrix.Nondegenerate.toBilin, SimpleGraph.adjMatrix_pow_apply_eq_card_walk, LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero, Matrix.trace_sum, LinearMap.toMatrix'_apply, UpperHalfPlane.σ_neg, Matrix.toLpLin_toLp, Matrix.transpose_sub, apply_eq_dotProduct_toMatrix₂_mulVec, instIsFiniteRelIndexGeneralLinearGroupAdjoinNegOne, kroneckerLinearEquiv_symm_kronecker, Matrix.isRightRegular_iff_vecMul_injective, IsSimpleRing.matrix, LinearMap.BilinForm.separatingRight_toMatrix_iff, Matrix.blockDiag'_one, ModularGroup.T_pow_mul_apply_one, summable_matrix_blockDiagonal', LinearMap.BilinForm.SeparatingLeft.toMatrix', LinearEquiv.mapMatrix_refl, Algebra.Norm.Transitivity.mul_auxMat_corner, UpperHalfPlane.coe_smul, Matrix.vecMulVec_eq, Matrix.isRepresentation.toEnd_exists_mem_ideal, ModularGroup.exists_row_one_eq_and_min_re, Matrix.projVandermonde_map, Matrix.ker_toLin_eq_bot, Matrix.transpose_natCast, Matrix.reindexAlgEquiv_mul, Matrix.trace_replicateCol_mul_replicateRow, Matrix.charpoly_one, Matrix.transpose_neg, Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff, Matrix.ofNat_fin_two, Matrix.inv_adjugate, AlgHom.mapMatrix_comp, pow_mulLeftLinearMap, Matrix.entryAddMonoidHom_apply, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', Matrix.det_one_add_X_smul, Matrix.nnnorm_replicateRow, Matrix.TransvectionStruct.mul_sumInl_toMatrix_prod, Matrix.permMatrix_one, AddEquiv.mapMatrix_apply, Matrix.det_reindex, Matrix.eRank_zero, LinearMap.toMatrix'_symm, Matrix.isStrictlyPositive_iff_posDef, Matrix.det_one_sub_mul_comm, Matrix.reindexLieEquiv_apply, LinearMap.mapMatrix_smul, Ideal.mem_matrix, Matrix.PosDef.commute_iff, Matrix.add_mul_mul_invOf_mul_eq_one', mulRightLinearMap_eq_zero_iff, Matrix.IsHermitian.cfcAux_apply, Matrix.UnitaryGroup.det_isUnit, Matrix.mul_eq_one_comm_of_card_eq, LieAlgebra.SpecialLinear.sl_bracket, Matrix.SpecialLinearGroup.scalar_eq_coe_self_center, linearMap_toMatrix_mul_basis_toMatrix, Matrix.conjTranspose_ratCast_smul, Matrix.rank_transpose_mul_self, Matrix.kroneckerTMulAlgEquiv_symm_apply, Matrix.ofLp_toEuclideanCLM, Matrix.conjTranspose_list_sum, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, Matrix.scalar_commute, Matrix.cons_transpose, LinearMap.toMatrix_transpose_apply, Matrix.exp_conjTranspose, Matrix.GeneralLinearGroup.ext_iff, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, Matrix.kroneckerTMulStarAlgEquiv_apply, Matrix.transposeRingEquiv_apply, AlgEquiv.mapMatrix_symm, Matrix.reindexLieEquiv_symm, IsUnit.det_zpow, toMatrix_dualTensorHom, Matrix.fromRows_mul_fromCols, MDifferentiable.slash, SimpleGraph.incMatrix_mul_transpose, IsCoprime.exists_SL2_row, Matrix.neg_mulVec, Matrix.SpecialLinearGroup.ext_iff, Matrix.instNormOneClassOfNonempty, Matrix.isElliptic_conj_iff, Matrix.range_toLin', Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, RootPairing.GeckConstruction.span_range_h_le_range_diagonal, Matrix.nonsing_inv_eq_ringInverse, Matrix.isSymm_mul_transpose_self, Matrix.blockDiag'_neg, Matrix.conjTranspose_eq_ofNat, CuspForm.coe_translate, Matrix.fromRows_one_isTotallyUnimodular_iff, Matrix.det_fromBlocks₁₁, LinearMap.mul_toMatrix', Matrix.liftLinear_apply, Matrix.Commute.zpow_zpow_self, IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing, evalRingHom_mapMatrix_comp_compRingEquiv, Matrix.instFiniteElemRealSpectrum, Matrix.instStarModule, Matrix.PosSemidef.add, Matrix.of_apply, exteriorPower.ιMultiDual_apply_ιMulti, Matrix.diagonal_kroneckerTMul, pow_mulRightLinearMap, Matrix.l2_opNNNorm_mul, RingEquiv.map_det, LinearMap.toMatrix_smulBasis_right, Matrix.toLpLin_symm_id, Matrix.range_toLin_eq_top, Matrix.UnitaryGroup.inv_val, HasSum.matrix_diagonal, Matrix.toLin_finTwoProd_apply, Matrix.isPositive_toEuclideanLin_iff, Matrix.nnnorm_entry_le_entrywise_sup_nnnorm, Matrix.subsingleton, Matrix.diagonal_fin_one, MatrixModCat.mem_toModuleCatObj, Matrix.add_mul_mul_mul_invOf_eq_one, Matrix.exp_transpose, CStarMatrix.reindexₐ_apply, Matrix.scalarAlgHom_apply, CStarMatrix.ofMatrix_eq_ofMatrixL, exteriorPower.pairingDual_ιMulti_ιMulti, LinearMap.mul_toMatrix₂, mem_skewAdjointMatricesLieSubalgebra, Matrix.det_fromBlocks_one₁₁, Matrix.blockDiagonal'_mul, Matrix.lieConj_symm_apply, Matrix.val_planeConformalMatrix, kroneckerTMulLinearEquiv_mul, QuadraticMap.discr_comp, Module.Basis.linearMap_repr_apply, Ideal.matrix_top, Matrix.hadamard_one_eq_one_iff, kroneckerTMulLinearEquiv_symm_kroneckerTMul, IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite, Matrix.isHermitian_inv, RootPairing.GeckConstruction.ω_mul_h, Matrix.traceLinearMap_apply, Matrix.linearIndependent_cols_iff_isUnit, Matrix.dualNumberEquiv_symm_apply, LinearMap.toMatrix'_mul, Matrix.cons_mul, mul_basis_toMatrix, RingCon.ofMatrix_rel', Matrix.one_hadamard_eq_one_iff, Subgroup.isArithmetic_iff_finiteIndex, Matrix.proj_comp_diagLinearMap, Matrix.evalAddMonoidHom_comp_diagAddMonoidHom, Matrix.matPolyEquiv_charmatrix, Matrix.invOf_fromBlocks_zero₁₂_eq, Matrix.single_mul_single_same, Matrix.isIrreducible_iff_exists_pow_pos, Matrix.diagonal_injective, Matrix.star_mul, RootPairing.GeckConstruction.instIsIrreducible, Matrix.SpecialLinearGroup.toGL_injective, LinearMap.toMatrix_algebraMap, Matrix.transpose_zpow, LinearMap.spectrum_toMatrix, Matrix.Module.instIsScalarTowerForall, Matrix.transpose_invOf, Matrix.norm_transpose, LinearMap.SeparatingRight.toMatrix₂, Matrix.one_submatrix_mul, Matrix.diagonal_mul, Matrix.smul_eq_mul_diagonal, Matrix.isUnit_toLin_iff, Matrix.posDef_iff_eq_conjTranspose_mul_self, Matrix.uniqueLinearEquiv_apply, Matrix.reindex_updateRow, Matrix.charmatrix_natCast, Matrix.one_apply_ne', Matrix.Module.scalar_smul, ModuleCat.matrixEquivalence_unitIso, Matrix.diagonal_toLin', Matrix.vandermonde_mul_vandermonde_transpose, Matrix.adjugate_smul, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, Matrix.charpoly_toLin', LinearMap.BilinForm.toMatrix_symm, Matrix.zpow_add_of_nonpos, Matrix.toLinearMap₂'_toMatrix', Matrix.toLinearMapₛₗ₂'_apply, Matrix.single_hadamard_single_of_ne, Matrix.replicateCol_mulVec, EisensteinSeries.vecMul_SL2_mem_gammaSet, Matrix.toLin'_pow, Matrix.conjTranspose_eq_intCast, Subalgebra.coe_matrix, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower_1, LinearMap.BilinForm.SeparatingLeft.toMatrix, Matrix.rank_zero, Subgroup.instHasDetOneMinGeneralLinearGroup, Matrix.submonoidCenter_eq_scalar_map, instIsNoetherianRingMatrix, Matrix.empty_mul_empty, CStarMatrix.smul_of, Matrix.toLinAlgEquiv'_apply, isCusp_SL2Z_iff, Matrix.IsHermitian.commute_iff, Matrix.l2_opNNNorm_def, Matrix.entryAddMonoidHom_toAddHom, apply_eq_star_dotProduct_toMatrix₂_mulVec, LinearMap.toMatrix_mul, Matrix.replicateRow_eq_zero, LinearMap.toMatrix₂_compl₁₂, TwoSidedIdeal.coe_equivMatrix_symm_apply, Matrix.minpoly_toLin', Matrix.vecMul_conjTranspose_mul_self_eq_zero, Matrix.nonsing_inv_apply, CategoryTheory.HomOrthogonal.matrixDecomposition_comp, LieAlgebra.Orthogonal.s_as_blocks, ModularForm.slash_action_eq'_iff, BilinForm.toMatrix_compRight, LinearMap.BilinForm.nondegenerate_toMatrix'_iff, Matrix.trace_conjTranspose_mul_self_eq_zero_iff, Algebra.smulTower_leftMulMatrix, LinearMap.toMatrix₂_toLinearMap₂, LinearMap.detAux_def', LinearMap.toMatrix_transpose_apply', Matrix.circulant_zero, surjective_cosetToCuspOrbit, Matrix.submatrix_id_mul_left, Matrix.one_hadamard, LinearMap.toMatrix'_intrinsicStar, Matrix.compLinearEquiv_symm_apply, Matrix.mem_range_scalar_iff_commute_single', Matrix.map_op_smul', Matrix.adjugate_mul_distrib, IsBaseChange.linearMapLeftRightHom_toMatrix, Matrix.mul_fromCols, Matrix.norm_replicateRow, Matrix.transpose_mem_rowStochastic_iff_mem_colStochastic, LinearMap.BilinForm.toMatrixAux_apply, Matrix.zero_hadamard, CongruenceSubgroup.strictWidthInfty_Gamma1, Matrix.isUnit_fromBlocks_iff_of_invertible₂₂, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, UpperHalfPlane.J_smul, Matrix.fromBlocks_diagonal, Matrix.single_mul_mul_single, Matrix.SpecialLinearGroup.SL2_inv_expl, Matrix.conjTransposeAddEquiv_apply, Module.finrank_matrix, instContinuousAddMatrix, LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv', LinearMap.toMatrix_smulRight, Matrix.adjugate_adjugate', Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one, kroneckerTMulLinearEquiv_tmul, Matrix.mem_specialUnitaryGroup_iff, LinearMap.toMatrix₂Aux_eq, Matrix.diagonalAddMonoidHom_apply, CartanMatrix.A_three, EisensteinSeries.eisensteinSeries_SIF_apply, Matrix.mul_invOf_cancel_right, LinearMap.mapMatrix_comp, vecMulVecBilin_apply_apply, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, isAdjointPair_toLinearMap₂', Matrix.cRank_reindex, Matrix.col_eq_transpose, Matrix.toLin'_apply', Matrix.lie_apply, Matrix.smulCommClass, LinearMap.toMatrix₂_symm, Matrix.vec_eq_zero_iff, Matrix.swap_mul_apply_right, Matrix.ker_toLin'_eq_bot_iff, Matrix.algebraMap_eq_diagonal, Matrix.PosSemidef.isUnit_sqrt_iff, Polynomial.sylvester_map_map, Matrix.kroneckerTMul_add, LinearMap.SeparatingLeft.toMatrix₂, LinearMap.toMatrix'_toLinearMap₂', Matrix.cRank_one, Matrix.reindexAlgEquiv_symm, Matrix.rank_reindex, Matrix.PosSemidef.zero, IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed, UpperHalfPlane.denom_neg, BilinForm.toMatrix_mul_basis_toMatrix, Matrix.piAddEquiv_symm_apply, Matrix.lift_cRank_reindex, LinearMap.BilinForm.mul_toMatrix', Matrix.mul_sub, Matrix.charpoly_units_conj, Matrix.fromBlocks_eq_of_invertible₂₂, FiniteField.Matrix.charpoly_pow_card, Matrix.SpecialLinearGroup.coe_inv, Matrix.UnitaryGroup.mul_val, Matrix.kronecker_assoc, Matrix.toLinearMap₂_symm, Matrix.trace_fin_one_of, Matrix.GeneralLinearGroup.isParabolic_conj_iff', AddMonoidHom.mapMatrix_neg, AddSubgroup.coe_matrix, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, CongruenceSubgroup.finiteIndex_conjGL, Matrix.sub_scalar_sq_eq_disc, LinearMap.toMatrixAlgEquiv_symm, Matrix.rank_self_mul_conjTranspose, LinearMap.toMatrixRight'_id, Matrix.IsHermitian.eigenvectorUnitary_apply, Matrix.isUnit_iff_isUnit_det, Matrix.mem_rowStochastic_iff_sum, FiniteField.trace_pow_card, IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite, Matrix.num_ofNat, IsCoprime.exists_SL2_col, LinearMap.minpoly_toMatrix, matrixEquivTensor_apply_single, Matrix.SpecialLinearGroup.range_toGL, Matrix.diagAddMonoidHom_apply, CStarMatrix.ofMatrix_symm_apply, Matrix.Nondegenerate.mul_iff_right, Matrix.conjTransposeRingEquiv_symm_apply, Matrix.nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂, LinearEquiv.mapMatrix_trans, matPolyEquiv_map_C, Matrix.SpecialLinearGroup.isEmbedding_toGL, LinearMap.toMatrixOrthonormal_apply, Matrix.frobenius_nnnorm_replicateRow, Matrix.replicateRow_mul_replicateCol, Algebra.leftMulMatrix_complex, Matrix.trace_single_mul, Algebra.Norm.Transitivity.eval_zero_comp_det, Matrix.blockDiag'_add, Matrix.schur_complement_eq₁₁, Matrix.transpose_injective, Matrix.det_mul, Matrix.IsHermitian.spectrum_eq_image_range, Matrix.invOf_add_mul_mul, Matrix.Pivot.mul_listTransvecRow_last_row, Matrix.hadamard_zero, Matrix.add_mul, Matrix.SpecialLinearGroup.coe_GLPos_neg, Matrix.conjTranspose_one, Matrix.vec_vecMul_kronecker_of_commute, MatrixEquivTensor.invFun_smul, Matrix.frobenius_nnnorm_replicateCol, Matrix.UnitaryGroup.mul_apply, Matrix.submatrix_one, Matrix.linftyOpNormSMulClass, Matrix.sum_mul, Matrix.mul_inv_cancel_left_of_invertible, Algebra.toMatrix_lmul', mem_skewAdjointMatricesSubmodule, mem_doublyStochastic_iff_mem_rowStochastic_and_mem_colStochastic, Matrix.det_fromBlocks_one₂₂, Matrix.isUnit_fromBlocks_zero₁₂, Matrix.blockDiagonal_smul, Matrix.det_nonsing_inv_mul_det, Matrix.blockDiagonal'AddMonoidHom_apply, Matrix.SpecialLinearGroup.coe_pow, Matrix.blockDiagonal_mul, Matrix.instT0Space, Continuous.matrix_replicateRow, Matrix.ker_diagonal_toLin', AffineBasis.toMatrix_inv_vecMul_toMatrix, Matrix.zpow_add_one, Matrix.nnnorm_transpose, RingEquiv.mapMatrix_apply, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, Matrix.subsemigroupCenter_eq_scalar_map, Matrix.blockDiagonal'_zero, SymplecticGroup.mem_iff', Matrix.num_natCast, Matrix.blockDiag'_smul, matrixEquivTensor_apply_symm, Matrix.kronecker_one, Matrix.toBilin'_apply, Matrix.mul_add, Matrix.adjugate_def, Matrix.isUnit_fromBlocks_iff_of_invertible₁₁, Matrix.UnitaryGroup.ext_iff, Ideal.matrix_jacobson_le, Matrix.exists_left_inverse_iff_isUnit, ModularForm.SL_slash_def, LinearMap.toMatrix_prodMap, Matrix.vecMul_add, Matrix.toLin_apply, Matrix.toLin'_one, Matrix.vecMul_injective, AddMonoidHom.mapMatrix_apply, Matrix.Module.smul_apply, continuous_matrix_diag, OnePoint.smul_infty_eq_ite, Matrix.vec_zero, MatrixEquivTensor.left_inv, Matrix.vecMul_surjective_iff_exists_left_inverse, Algebra.smulTower_leftMulMatrix_algebraMap_ne, Matrix.fromBlocks_one, Matrix.posDef_sum, Matrix.diagonal_mul_diagonal', doublyStochastic_eq_convexHull_permMatrix, Matrix.frobenius_nnnorm_diagonal, eval_det, Matrix.reindexLinearEquiv_mul, Matrix.blockDiagonal_sub, Matrix.circulant_mul, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, Matrix.comp_symm_diagonal, Matrix.conjTranspose_zpow, RingHom.map_adjugate, Matrix.PosDef.fromBlocks₂₂, Matrix.toLin_conjTranspose, mulRightLinearMap_apply, Matrix.zero_le_one_row, Matrix.IsHermitian.spectral_theorem, Matrix.IsHermitian.inv, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, Module.Basis.continuous_toMatrix, Matrix.diagonalAlgHom_apply, rank_matrix_module', Matrix.add_hadamard, Matrix.smul_kronecker, Matrix.PosSemidef.sq_sqrt, Matrix.kronecker_ofNat, Matrix.GeneralLinearGroup.mem_center_iff_val_eq_scalar, UpperHalfPlane.coe_J_smul, Matrix.mul_adjp_apply_eq, RootPairing.GeckConstruction.ωConj_invFun, Matrix.map_add, Matrix.Commute.self_zpow, endVecAlgEquivMatrixEnd_apply_apply, Int.Matrix.one_le_norm_A_of_ne_zero, Matrix.blockDiagonal'_add, Matrix.single_mul_single_of_ne, Matrix.one_hadamard_eq_zero_iff, Matrix.norm_conjTranspose, Matrix.transposeAddEquiv_apply, NumberField.conj_basisMatrix, Matrix.GeneralLinearGroup.map_swap, Matrix.trace_toLin'_eq, Matrix.vecMul_sum, Matrix.one_kronecker_one, PEquiv.single_mul_single_right, Matrix.submatrix_one_equiv, Orientation.rotation_eq_matrix_toLin, Matrix.mul_submatrix_one, NumberField.Units.abs_det_eq_abs_det, Matrix.trace_list_sum, CongruenceSubgroup.strictPeriods_Gamma1, Matrix.trace_add, Matrix.subsingleton_of_empty_left, CartanMatrix.A_two, Matrix.PosDef.isStrictlyPositive, Matrix.kroneckerMap_smul_left, Matrix.scalar_comm_iff, IsSemisimpleModule.exists_end_ringEquiv, OnePoint.IsBoundedAt.smul_iff, Matrix.Pivot.listTransvecCol_mul_last_row_drop, Matrix.transpose_intCast, AlgHom.mapMatrix_id, Matrix.add_mul_mul_mul_invOf_eq_one', LinearEquiv.isUnit_det, Matrix.mvPolynomialX_mapMatrix_eval, CartanMatrix.D_two, Matrix.single_mul_eq_updateRow_zero, Matrix.blockDiag'AddMonoidHom_apply, Matrix.IsHermitian.eigenvectorUnitary_coe, Matrix.PosSemidef.zpow, Matrix.nonsing_inv_cancel_or_zero, Algebra.trace_eq_matrix_trace, Matrix.isHermitian_add_transpose_self, Matrix.inv_pow', mem_selfAdjointMatricesSubmodule, Matrix.diagonal_sub, Algebra.traceMatrix_of_basis, RingCon.matrix_injective, NumberField.inverse_basisMatrix_mulVec_eq_repr, matPolyEquiv_symm_C, Matrix.spectrum_toLin, LinearMap.mapMatrixModule_comp, LinearMap.toMatrix'_comp, Matrix.toLinearEquiv'_apply, LinearMap.isUnit_toMatrix'_iff, Matrix.toBilin_toMatrix, Matrix.blockDiagonal_zero, Matrix.GeneralLinearGroup.coe_inv, Matrix.nondegenerate_toLinearMap₂_iff, SlashInvariantForm.coe_trace, IsSemisimpleRing.instMatrix, Matrix.nonsing_inv_apply_not_isUnit, Matrix.reindexLinearEquiv_apply, Matrix.toBilin'_comp, Matrix.isHermitian_iff_isSymmetric, Matrix.PosSemidef.inv_sqrt, LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal', instIsTopologicalAddGroupMatrix, Matrix.PosDef.add_posSemidef, RingCon.matrix_bot, Matrix.inv_mul_cancel_right_of_invertible, Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row, Matrix.linfty_opNorm_mulVec, Matrix.compAlgEquiv_symm_apply, Matrix.det_neg, Matrix.finite_real_spectrum, Matrix.discr_conj', Matrix.replicateRow_vecMul, Module.Free.matrix, Matrix.den_intCast, Matrix.mul_swap_of_ne, Matrix.PosSemidef.pow, Matrix.isUnit_comp_iff, Matrix.norm_lt_iff, Module.Basis.end_repr_symm_apply, Matrix.blockDiagonal_add, InnerProductSpace.toMatrix_rankOne, Matrix.uniqueRingEquiv_symm_apply, RingHom.map_det, RingCon.matrix_apply_single, Matrix.exp_blockDiagonal, rank_matrix', Module.Basis.toMatrix_mul_toMatrix_flip, CStarMatrix.reindexₗ_apply, Matrix.ext_linearMap_iff, Matrix.map_natCast, LinearMap.mul_toMatrix₂_mul, Matrix.isUnit_conjTranspose, Matrix.transpose_tsum, Matrix.mul_inv_rev, mem_skewAdjointMatricesLieSubalgebra_unit_smul, CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv, exteriorPower.alternatingMapToDual_apply_ιMulti, Matrix.toBlock_inverse_eq_zero, Matrix.mul_right_eq_iff_eq_mul_invOf, SlashInvariantForm.slash_action_eqn_SL'', Matrix.mul_nonsing_inv_cancel_right, Matrix.vecMulVec_zero, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, CongruenceSubgroup.strictWidthInfty_Gamma, Matrix.diagonal_one, Matrix.nnnorm_conjTranspose, Matrix.vecMul_vecMul, IsSemisimpleModule.exists_end_algEquiv, Matrix.stdBasis_eq_single, RootPairing.GeckConstruction.isNilpotent_f, Matrix.toLpLinAlgEquiv_apply_apply_ofLp, LinearMap.toMatrix'_id, Matrix.star_eq_inv, Matrix.submatrix_one_embedding, ModuleCat.matrixEquivalence_counitIso, Matrix.inv_kronecker, Matrix.toLinearMapₛₗ₂_symm, Matrix.zpow_mul', Matrix.diagonal_kronecker, RootPairing.GeckConstruction.lie_e_f_same, LinearMap.BilinForm.mul_toMatrix_mul, Matrix.traceAddMonoidHom_apply, Matrix.conjTranspose_eq_one, Matrix.mul_swap_apply_left, Matrix.posSemidef_sum, Matrix.circulant_mul_comm, Matrix.posSemidef_intCast_iff, RootPairing.GeckConstruction.ω_mul_ω, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix, RootPairing.GeckConstruction.f_lie_v_ne, Matrix.toLinAlgEquiv_apply, Matrix.exp_units_conj', Matrix.IsPrimitive.exists_pos_pow, LinearMap.nondegenerate_toMatrix₂'_iff, LieAlgebra.matrix_trace_commutator_zero, LinearMap.BilinForm.toMatrix'_comp, LinearMap.mapMatrix_apply, Algebra.Norm.Transitivity.mul_auxMat_blockTriangular, EisensteinSeries.q_expansion_bernoulli, mulLinearMap_apply_apply, UpperHalfPlane.coe_specialLinearGroup_apply, Matrix.linfty_opNorm_replicateCol, Matrix.pow_sub', Topology.IsInducing.matrix_map, Algebra.smulTower_leftMulMatrix_algebraMap, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, Matrix.transpose_one, Matrix.add_kroneckerTMul, Matrix.det_smul_adjugate_adjugate, RootPairing.GeckConstruction.ωConj_toFun, Matrix.piEquiv_symm_apply, TwoSidedIdeal.orderIsoMatrix_symm_apply_ringCon_r, SimpleGraph.adjMatrix_mul_apply, Matrix.charpoly_fromBlocks_zero₁₂, Matrix.toLinearMapRight'_apply, LinearMap.BilinForm.toMatrix_mul, MatrixModCat.isScalarTower_toModuleCat, rank_matrix, RootPairing.GeckConstruction.e_lie_v_ne, Matrix.diagonalRingHom_apply, Matrix.instIsScalarTowerForall, Matrix.posSemidef_iff_eq_sum_vecMulVec, Matrix.GeneralLinearGroup.map_mul_map_inv, LieAlgebra.SpecialLinear.val_single, Matrix.ofLp_toEuclideanLin_apply, Matrix.det_reindex_self, Matrix.toLinearMap₂_apply, Matrix.invOf_diagonal_eq, Matrix.vec_vecMul_kronecker, Matrix.mem_orthogonalGroup_iff, Matrix.IsTotallyUnimodular.reindex, Matrix.transpose_pow, Matrix.GeneralLinearGroup.val_inv_det_apply, Matrix.isHermitian_transpose_add_self, Matrix.inv_mul_of_invertible, Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow, Matrix.reindexAlgEquiv_refl, RootPairing.GeckConstruction.ω_mul_e, Matrix.Module.single_smul, SimpleGraph.incMatrix_mul_transpose_diag, Matrix.isHermitian_natCast, mulLeftLinearMap_eq_mulLeft, Matrix.transpose_mem_matrix_iff, CongruenceSubgroup.Gamma1_mem, RootPairing.GeckConstruction.isNilpotent_e, Matrix.GeneralLinearGroup.center_eq_range_units, Matrix.adjugate_zero, Matrix.swap_mul_of_ne, Matrix.SpecialLinearGroup.coe_transpose, LinearMap.nondegenerate_toLinearMap₂'_iff_det_ne_zero, Matrix.mulVecBilin_apply, Matrix.mul_empty, Matrix.add_vecMulVec, lieEquivMatrix'_symm_apply, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing, Matrix.zpow_neg, Matrix.dotProduct_vecMul_hadamard, Matrix.proj_diagonal, ModularGroup.im_smul_eq_div_normSq, Matrix.self_mul_conjTranspose_mulVec_eq_zero, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, Matrix.eval_charpoly, Matrix.SpecialLinearGroup.coe_GL_coe_matrix, extremePoints_doublyStochastic, Matrix.det_fromBlocks₂₂, LieAlgebra.Orthogonal.jd_transform, Matrix.linfty_opNNNorm_mul, LinearMap.isUnit_toMatrix_iff, Matrix.map_mul_intCast, Matrix.mul_left_eq_iff_eq_invOf_mul, LinearMap.BilinForm.toMatrix_compLeft, Matrix.diag_add, LinearMap.trace_eq_matrix_trace, BilinForm.toMatrix_apply, Continuous.matrix_diagonal, Matrix.vecMul_natCast, Matrix.BlockTriangular.sub_iff_left, Matrix.linfty_opNorm_toMatrix, Matrix.toBilin'_apply', Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, Matrix.smul_mul, Matrix.replicateCol_smul, Matrix.fromCols_mul_fromRows_eq_one_comm, Matrix.toLinearMap₂'_single, Matrix.Pivot.mul_listTransvecRow_last_col_take, matPolyEquiv_eval_eq_map, Matrix.smul_eq_mulVec, RootPairing.GeckConstruction.h_mem_lieAlgebra, Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero, LinearMap.separatingRight_toLinearMap₂'_of_det_ne_zero', CongruenceSubgroup.mem_conjGL, Matrix.det_fromBlocks_zero₁₂, mulLeftLinearMap_one, Matrix.frobenius_norm_mul, matPolyEquiv_coeff_apply, LinearMap.BilinForm.mul_toMatrix, Matrix.piAlgEquiv_symm_apply, Matrix.vecMul_injective_iff_isUnit, Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues, Matrix.normSMulClass, Matrix.reindex_symm, Matrix.GeneralLinearGroup.coe_map_mul_map_inv, Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det, Matrix.of_mem_specialOrthogonalGroup_fin_two_iff, Matrix.reindexLinearEquiv_symm, Matrix.SpecialLinearGroup.toLin'_to_linearMap, LinearMap.mul_toMatrix₂'_mul, LinearMap.toMatrix₂'_mul, Matrix.instIsOrderedAddMonoid, Matrix.mem_colStochastic, Matrix.det_mul_add_one_comm, OnePoint.smul_infty_def, Matrix.conjTranspose_pow, Algebra.toMatrix_lsmul, toMatrix_innerSL_apply, Matrix.diag_neg, Matrix.kronecker_mulVec_vec, Matrix.separatingLeft_toLinearMap₂'_iff, Matrix.linfty_opNormOneClass, Matrix.linfty_opNorm_mul, LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero', Matrix.mem_colStochastic_iff_sum, Matrix.comp_map_map, Matrix.charpoly_mul_comm, PiLp.basis_toMatrix_basisFun_mul, instContinuousNegMatrix, Matrix.tail_transpose, Matrix.isRepresentation.toEnd_surjective, BilinForm.toMatrix_mul, Matrix.SpecialLinearGroup.SL2_inv_expl_det, Matrix.isDiag_smul_one, Matrix.linfty_opNNNorm_replicateCol, CongruenceSubgroup.strictPeriods_Gamma, LinearMap.toMatrix_comp, Matrix.row_eq_self, ModularGroup.tendsto_lcRow0, Matrix.submatrixEquivInvertibleEquivInvertible_apply, cosetToCuspOrbit_apply_mk, Matrix.toLinAlgEquiv_self, instIsTopologicalSemiringMatrix, Matrix.kroneckerMapBilinear_mul_mul, Matrix.detp_mul, Matrix.instIsUniformAddGroup, Matrix.det_mul_column, Matrix.separatingLeft_toBilin'_iff, Matrix.kroneckerAlgEquiv_symm_apply, Topology.IsOpenEmbedding.matrix_map, Matrix.charmatrix_one, Matrix.coeff_det_one_add_X_smul_one, Matrix.trace_toLin_eq, Matrix.isAddUnit_iff, LinearMap.toMatrix₂_mul_basis_toMatrix, Matrix.Pivot.listTransvecCol_mul_last_row, Matrix.conjTranspose_intCast_smul, Matrix.GeneralLinearGroup.val_inv_scalar_apply, Matrix.Represents.add, Module.Basis.toMatrix_eq_toMatrix_constr, Matrix.det_reindexLinearEquiv_self, Matrix.mul_eq_one_comm_of_equiv, Matrix.isUnit_nonsing_inv_iff, Matrix.lie_transpose, Matrix.isAdjMatrix_iff_hadamard, Matrix.num_one, SimpleGraph.incMatrix_transpose_mul_diag, OnePoint.exists_mem_SL2, Matrix.reindex_refl_refl, ModularGroup.abs_c_le_one, Matrix.mul_transpose_self_isDiag_iff_hasOrthogonalRows, Matrix.sub_mulVec, Matrix.blockTriangular_inv_of_blockTriangular, Matrix.nonsing_inv_mul_cancel_right, Matrix.diagonalInvertibleEquivInvertible_symm_apply, Matrix.instSMulCommClassForall, Matrix.kroneckerTMul_smul, Matrix.trace_mul_single, Matrix.kroneckerMap_assoc, Matrix.IsHermitian.cfcAux_id, Matrix.inv_zpow', Matrix.posDef_natCast_iff, Matrix.mem_glpos, Matrix.updateCol_zero_zero, mulRightLinearMap_mul, SL_reduction_mod_hom_val, Matrix.Represents.one, Matrix.Pivot.length_listTransvecCol, Subgroup.le_adjoinNegOne, Matrix.trace_transpose_mul, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, Matrix.blockDiagonal_pow, Polynomial.natDegree_det_X_add_C_le, Matrix.toBilin'Aux_eq, AlgEquiv.map_det, Matrix.one_fin_three, LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix', Matrix.toLin_finTwoProd_toContinuousLinearMap, Matrix.trace_one, Topology.IsEmbedding.matrix_map, Matrix.disc_conj, Matrix.kroneckerMap_smul_right, LinearMap.toMatrixAlgEquiv'_symm, Matrix.specialUnitaryGroup.coe_star, Matrix.toSquareBlockProp_def, Matrix.of_symm_single, Matrix.invOf_mul_cancel_right, Matrix.finiteDimensional, OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary, Matrix.transpose_smul, LinearMap.mapMatrix_id, Matrix.GeneralLinearGroup.val_map_apply, Matrix.single_eq_of_single_single, Matrix.matrixOfPolynomials_blockTriangular, Matrix.toBlock_one_self, LinearMap.mapMatrixModule_id, Matrix.uniqueAlgEquiv_symm_apply, Matrix.mul_invOf_cancel_left, Matrix.of_col, Matrix.transposeAlgEquiv_apply, Matrix.kroneckerTMulBilinear_apply, Matrix.uniqueLinearEquiv_symm_apply, mem_doublyStochastic, Matrix.sum_single_intCast, AffineBasis.isUnit_toMatrix_iff, Matrix.diag_one, Matrix.vecMul_sub, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, Matrix.conjTranspose_multiset_sum, Matrix.Nondegenerate.mul_iff_left, UpperHalfPlane.det_J, ModularGroup.coe_one, hasEigenvalue_toLin'_diagonal_iff, Matrix.circulant_single, Matrix.cRank_zero, Matrix.smul_hadamard, Matrix.IsHermitian.pow, LinearMap.toMatrix'_toLinearMapₛₗ₂', Matrix.Semiring.isScalarTower, Matrix.natCast_mulVec, Matrix.mem_unitaryGroup_iff', Matrix.diagonal_add, Matrix.inv_submatrix_equiv, Matrix.toLpLin_mul, Matrix.convex_rowStochastic, RootPairing.GeckConstruction.lie_h_f, Subsemiring.coe_matrix, ModularForm.coe_norm, Matrix.toLin'_submatrix, Matrix.J_inv, Matrix.conjTranspose_ofNat_smul, Matrix.map_intCast, CongruenceSubgroup.Gamma1_to_Gamma0_mem, isStablyFiniteRing_iff, RootPairing.GeckConstruction.ω_mul_f, Subgroup.strictPeriods_SL2Z, Matrix.separatingLeft_toLinearMap₂_iff, CongruenceSubgroup.mem_conjGL', Matrix.diagonalInvertibleEquivInvertible_apply, Matrix.subalgebraCenter_eq_scalarAlgHom_map, Matrix.toLin_toMatrix, LinearMap.toMatrix₂_apply, Matrix.uniformContinuous, PiToModule.fromMatrix_apply, Matrix.vecMulVec_eq_zero, Matrix.empty_mul, Matrix.frobeniusNormSMulClass, Matrix.toEuclideanLin_apply_piLp_toLp, Matrix.posDef_inv_iff, Matrix.trace_fin_three_of, FixedDetMatrices.smul_def, Matrix.blockDiag'_sub, Matrix.transpose_nonsing_inv, Matrix.mul_nonsing_inv_cancel_left, Matrix.map_smul', Matrix.isSymm_transpose_add_self, Matrix.IsHermitian.fromBlocks₁₁, Matrix.linfty_opNorm_eq_opNorm, Matrix.invertibleEquivDetInvertible_apply, Matrix.reindexAlgEquiv_apply, Matrix.hadamard_add, Algebra.traceMatrix_of_matrix_mulVec, Algebra.leftMulMatrix_mulVec_repr, Matrix.adjugate_subsingleton, Matrix.two_mul_expl, Matrix.topologicalRing, Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal, Matrix.conjTranspose_eq_zero, Matrix.invOf_add_mul_mul', Algebra.Norm.Transitivity.mul_auxMat_toSquareBlock_eq, ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, Matrix.det_matrixOfPolynomials, Matrix.mul_kroneckerTMul_mul, Matrix.reindex_trans, Subgroup.mem_strictPeriods_iff, Matrix.cramer_one, Matrix.of_row, Matrix.posDef_intCast_iff, Matrix.mul_right_injective_iff_mulVec_injective, Matrix.PosDef.mul_mul_conjTranspose_same, MatrixModCat.toModuleCat_map, Polynomial.toMatrix_sylvesterMap, RootPairing.GeckConstruction.lie_e_lie_f_apply, Matrix.det_fromBlocks_zero₂₁, Matrix.vecMulVec_mul_vecMulVec, Matrix.of_symm_apply, Matrix.dualNumberEquiv_apply, Matrix.det_one, Matrix.separatingRight_toBilin'_iff, Matrix.GeneralLinearGroup.val_swap, Matrix.isNilpotent_iff, Matrix.zero_mul, Matrix.toLin_finTwoProd, Matrix.adjugate_one, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, IsSimpleRing.exists_ringEquiv_matrix_divisionRing, EisensteinSeries.vecMulSL_gcd, Module.Basis.linearMap_repr_symm_apply, support_subset_support_matPolyEquiv, Matrix.toLinAlgEquiv'_toMatrixAlgEquiv', Matrix.permMatrix_mem_colStochastic, Matrix.mul_left_injective_iff_vecMul_injective, Matrix.IsSymm.neg, TwoSidedIdeal.matrix_monotone, ModularForm.prod_fintype_slash, Matrix.mul_fin_two, IsSMulRegular.matrix, Matrix.conjTranspose_neg, Matrix.kroneckerTMulAlgEquiv_apply, Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, Matrix.BlockTriangular.inv_toBlock, IsCompact.matrix, PEquiv.toMatrix_injective, matPolyEquiv_symm_map_eval, LDL.diag_eq_lowerInv_conj, endVecAlgEquivMatrixEnd_symm_apply_apply, Matrix.frobenius_norm_diagonal, Matrix.mem_specialOrthogonalGroup_fin_two_iff, Matrix.IsHermitian.eigenvalues_mem_spectrum_real, Matrix.commute_diagonal, LinearMap.nondegenerate_toMatrix₂_iff, Matrix.trace_kroneckerMapBilinear, Matrix.conjTranspose_list_prod, Matrix.blockDiag_sub, Matrix.updateRow_zero_mul_updateCol_zero, CStarMatrix.neg_of, Matrix.num_intCast, Matrix.GeneralLinearGroup.map_apply, Ideal.matrix_strictMono_of_nonempty, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower, Matrix.trace_smul, LinearMap.mapMatrix_add, AlgEquiv.mapMatrix_trans, Matrix.toLinAlgEquiv'_one, Matrix.replicateCol_eq_zero, Matrix.toLin_one, SlashInvariantForm.vAdd_width_periodic, Matrix.self_mul_conjTranspose_mul_eq_zero, UpperHalfPlane.denom_one, Matrix.isUnit_exp, Matrix.invOf_fromBlocks_zero₂₁_eq, Matrix.toLin_transpose, Matrix.det_mul_row, Matrix.IsTotallyUnimodular.one_fromCols, Complex.toMatrix_conjAe, Matrix.diagonal_neg, FixedDetMatrices.ext_iff, BilinForm.mul_toMatrix, Matrix.isHermitian_zero, Matrix.kroneckerMap_add_right, Matrix.invOf_submatrix_equiv_eq, Matrix.submatrix_mul_transpose_submatrix, Matrix.cons_vecMul, Matrix.rank_mul_le_left, MatrixEquivTensor.right_inv, Matrix.toLpLin_symm_comp, Matrix.det_one_add_replicateCol_mul_replicateRow, Algebra.Norm.Transitivity.eval_zero_det_det, Matrix.zero_zpow_eq, Matrix.toLinearMapₛₗ₂_apply_basis, Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec, convex_doublyStochastic, Matrix.det_fin_one_of, Matrix.mulVec_surjective_iff_exists_right_inverse, UpperHalfPlane.val_J, PEquiv.toMatrix_refl, matPolyEquiv_eval, RootPairing.GeckConstruction.f_lie_v_same, LinearMap.toMatrix_toSpanSingleton, Matrix.vecMulVec_cons, Matrix.det_mul_comm, LinearMap.toMatrix₂_symm', Matrix.conjTranspose_smul_non_comm, ModularGroup.coe_T, AlgEquiv.mopMatrix_symm_apply, Matrix.comp_symm_transpose, Matrix.nonsing_inv_mul_cancel_left, ModularForm.slash_def, mulLeftLinearMap_zero_eq_zero, Matrix.transpose_eq_zero, Matrix.isHermitian_one, Matrix.mulVec_surjective_iff_isUnit, Matrix.sum_single_natCast, LinearMap.Nondegenerate.toMatrix₂', UpperHalfPlane.instContinuousGLSMul, Matrix.cons_vecMul_cons, Matrix.kroneckerMap_zero_left, MatrixEquivTensor.invFun_zero, Matrix.IsSymm.inv, Matrix.charpoly.univ_map_eval₂Hom, Matrix.transposeAlgEquiv_symm_apply, Matrix.det_fin_two_of, Matrix.single_eq_updateCol_zero, Matrix.blockDiagonal'_sub, Matrix.Nondegenerate.toBilin', Matrix.kroneckerMap_zero_right, LinearMap.toMatrix_singleton, Matrix.mul_adjp_apply_ne, LinearMap.BilinForm.toMatrix'_mul, Matrix.det_neg_eq_smul, Matrix.blockDiagAddMonoidHom_apply, Matrix.sum_mulVec, Matrix.vecMulVec_neg, ModularForm.is_invariant_one', Matrix.map_smulₛₗ, Matrix.diag_list_sum, Matrix.diagonal_unique, MatrixModCat.toModuleCat_obj_isAddCommGroup, EisensteinSeries.eisensteinSeriesSIF_apply, Matrix.ofNat_kronecker, Matrix.zero_vecMulVec, Matrix.zpow_sub_one, Matrix.mul_one, LinearMap.toMatrix₂'_compl₂, UpperHalfPlane.mul_smul', Matrix.toLinAlgEquiv'_symm, Matrix.trace_sub, AddEquiv.mapMatrix_symm, Matrix.instIsScalarTowerMulOppositeForallOfSMulCommClass, Matrix.nnnorm_diagonal, Matrix.entryLinearMap_apply, Matrix.fromRows_mul, RingHom.mapMatrix_comp, Matrix.sum_single_eq_diagonal, Matrix.toLinearEquiv_kroneckerAlgEquiv, Matrix.diagonal_mul_diagonal, Matrix.mul_transvection_apply_of_ne, Matrix.sub_vecMulVec, Matrix.SpecialLinearGroup.coe_neg, Matrix.det_sum_smul_le, Matrix.det_mul_left_comm, Matrix.Module.diagonal_const_smul, Matrix.nondegenerate_toLinearMap₂'_iff, Matrix.fromCols_one_isTotallyUnimodular_iff, Matrix.TransvectionStruct.sumInl_toMatrix_prod_mul, LinearMap.separatingRight_toMatrix₂_iff, SymplecticGroup.coe_inv', Matrix.neg_mul, Matrix.IsHermitian.star_mul_self_mul_eq_diagonal, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing, Matrix.charpoly_mul_comm', Equiv.mapMatrix_refl, Matrix.conjTranspose_mul_self_eq_zero, Matrix.mulVecLin_reindex, Matrix.l2_opNNNorm_diagonal, Matrix.instCStarRing, Matrix.IsHermitian.eigenvectorUnitary_transpose_apply, Matrix.replicateRow_mul_replicateCol_apply, Matrix.GeneralLinearGroup.map_one, Matrix.permanent_zero, Matrix.vecMulVec_smul, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, Matrix.cramer_smul, Matrix.GeneralLinearGroup.map_mul, Matrix.UnitaryGroup.toLin'_mul, PEquiv.toMatrix_mul_apply, Matrix.cons_mulVec, Matrix.conjTranspose_rat_smul, Matrix.mul_fin_three, CStarMatrix.uniformEmbedding_ofMatrix, SimpleGraph.adjMatrix_mul_self_apply_self, Matrix.neg_vecMulVec, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite, Matrix.fromBlocks_smul, Matrix.trace_surjective, Matrix.SpecialLinearGroup.coe_matrix_coe, FixedDetMatrices.smul_coe, Matrix.reindexLinearEquiv_refl_refl, instT2SpaceMatrix, Matrix.SpecialLinearGroup.mapGL_coe_matrix, Matrix.nnnorm_def, Matrix.inv_zpow, Matrix.coe_det_isEmpty, IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed, Matrix.mul_left_injective_of_invertible, Matrix.isDiag_fromBlocks_iff, AddEquiv.mapMatrix_refl, Algebra.Norm.Transitivity.auxMat_toSquareBlock_ne, matPolyEquiv_symm_X, Matrix.comp_diagonal, Matrix.GeneralLinearGroup.coe_mul, Matrix.frobenius_nnnorm_def, OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose, LinearMap.separatingLeft_toMatrix₂_iff, Matrix.pow_inv_comm', Matrix.blockDiag_smul, Module.Finite.matrix, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, SimpleGraph.one_add_adjMatrix_add_compl_adjMatrix_eq_allOnes, AddMonoidHom.mapMatrix_add, Matrix.trace_zero, Matrix.IsHermitian.eigenvalues_eq_zero_iff, Matrix.det_units_conj, LinearMap.BilinForm.toMatrix'_toBilin', Matrix.aeval_self_charpoly, Matrix.mem_orthogonalGroup_iff', Matrix.conjTransposeRingEquiv_apply, Matrix.nnnorm_le_iff, Matrix.compRingEquiv_apply, TwoSidedIdeal.asIdeal_matrix, LieAlgebra.Orthogonal.pso_inv, Matrix.map_smul, Matrix.blockDiagonalRingHom_apply, Matrix.conjTranspose_smul, LinearMap.det_toMatrix', Matrix.separatingLeft_toBilin_iff, Module.Basis.toMatrix_reindex', LinearMap.Nondegenerate.toMatrix₂, Matrix.map_pow, Matrix.rank_mul_eq_left_of_isUnit_det, Subgroup.IsArithmetic.finiteIndex_comap, LinearMap.toMatrixAlgEquiv_apply', Matrix.transpose_mul_self_isDiag_iff_hasOrthogonalCols, IsLeftRegular.matrix, Matrix.Represents.mul, Matrix.SpecialLinearGroup.det_mapGL, mulLeftLinearMap_eq_zero_iff, Matrix.smul_single, transpose_mem_doublyStochastic_iff, Matrix.num_eq_zero_iff, Matrix.replicateCol_vecMul, Matrix.intCast_apply, Matrix.submatrix_mul_equiv, ModularForm.SL_slash_apply, Matrix.disc_conj', LinearMap.BilinForm.Nondegenerate.toMatrix', Matrix.of_sub_of, Matrix.charpoly_reindex, Matrix.fromBlocks_multiply, Matrix.trace_mul_cycle, Matrix.TransvectionStruct.reverse_inv_prod_mul_prod, Matrix.charP, LinearMap.toMatrix_basis_equiv, Matrix.UnitaryGroup.toGL_one, Matrix.fromBlocks_zero, Matrix.reindexLinearEquiv_comp_apply, OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self, Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange, AffineBasis.toMatrix_self, Matrix.den_one, CartanMatrix.A_one, EisensteinSeries.eisSummand_SL2_apply, OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal, Matrix.vecMul_self_mul_conjTranspose_eq_zero, Matrix.adjugate_fin_zero, Matrix.scalar_apply, Matrix.SeparatingRight.toBilin', Matrix.kroneckerTMul_assoc, Matrix.PosSemidef.sqrt_mul_self, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, Matrix.range_diagonal, Matrix.one_apply_eq, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, Matrix.piLinearEquiv_symm_apply, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, Matrix.diag_sum, mulLeftLinearMap_apply, Matrix.isHermitian_mul_mul_conjTranspose, Matrix.zpow_one_add, RingEquiv.mapMatrix_refl, Matrix.PosDef.intCast, Matrix.single_mul_apply_of_ne, BilinForm.toMatrix_compLeft, Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace, Matrix.isUnit_transpose, Matrix.isSymm_one, Matrix.trace_units_conj', RootPairing.GeckConstruction.f_mem_lieAlgebra, Ideal.matrix_bot, Matrix.mem_rowStochastic, LinearMap.toMatrix₂'_comp, mulLeftLinearMap_mul, Matrix.toLinearMap₂_apply_basis, Matrix.PosSemidef.smul, Matrix.coe_ofLinearEquiv_symm, Matrix.IsSymm.sub, Matrix.exp_blockDiagonal', LinearMap.toMatrix_pow, ModularGroup.det_coe, Matrix.diagonal_tsum, Matrix.IsHermitian.sub, mem_selfAdjointMatricesSubmodule', LinearMap.BilinForm.toMatrix_comp, Matrix.SpecialLinearGroup.toLin'_symm_apply, Matrix.l2_opNNNorm_conjTranspose_mul_self, Matrix.swap_mul_apply_left, Ideal.matrix_monotone, ModularGroup.coe_T_zpow, Matrix.trace_map, Matrix.natCast_kronecker_natCast, TwoSidedIdeal.matrix_ringCon, LieAlgebra.Orthogonal.indefiniteDiagonal_transform, Matrix.GeneralLinearGroup.val_inv_swap, Matrix.uniqueEquiv_apply, Matrix.intCast_mulVec, UpperHalfPlane.denom_cocycle', RootPairing.GeckConstruction.e_mem_lieAlgebra, ModularGroup.lcRow0_apply, Matrix.BlockTriangular.sub, IsStablyFiniteRing.isDedekindFiniteMonoid, LinearMap.toMatrix'_one, LieAlgebra.SpecialLinear.val_singleSubSingle, Matrix.one_kroneckerTMul_one, Algebra.smulTower_leftMulMatrix_algebraMap_eq, Matrix.transpose_mem_colStochastic_iff_mem_rowStochastic, Matrix.cstar_norm_def, LieAlgebra.Orthogonal.pb_inv, Matrix.invOf_eq, Matrix.blockDiagonalAddMonoidHom_apply, ModularForm.coe_translate, Matrix.diagonal_fin_three, Matrix.trace_neg, Matrix.isHermitian_transpose_mul_self, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, RootPairing.GeckConstruction.lie_h_h, CStarMatrix.of_zero, Matrix.TransvectionStruct.toMatrix_sumInl, Matrix.vec_mul_eq_vecMul, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, Matrix.Fin.circulant_injective, Matrix.IsTotallyUnimodular.fromRows_one, Matrix.comp_symm_apply, NumberField.Units.finrank_mul_regulator_eq_det, Matrix.den_neg, inner_matrix_row_row, Matrix.adjugate_pow, UpperHalfPlane.neg_smul, Matrix.toMvPolynomial_mul, Matrix.map_mul, Matrix.transpose_empty_rows, basis_toMatrix_mul_linearMap_toMatrix, Matrix.zpow_mul, LinearMap.toMatrixₛₗ₂'_apply, Matrix.piEquiv_apply, Matrix.GeneralLinearGroup.val_scalar_apply, skewAdjointMatricesLieSubalgebraEquiv_apply, Matrix.toLinearMapRight'_one, Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace, Matrix.conjTranspose_mul_self_mul_eq_zero, Matrix.fromCols_mul_fromRows, Matrix.invertibleEquivDetInvertible_symm_apply, LinearMap.toMatrixAlgEquiv_reindexRange, Matrix.GeneralLinearGroup.map_id, Matrix.comp_map_transpose, permMatrix_mem_doublyStochastic, Matrix.blockDiag_neg, Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, Matrix.submatrixEquivInvertibleEquivInvertible_symm_apply, Matrix.instStarOrderedRing, Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix, CStarMatrix.of_add_of, Matrix.vecMul_mulVec, AffineBasis.isUnit_toMatrix, AddSubmonoid.coe_matrix, Matrix.linfty_opNNNorm_replicateRow, ModularForm.coe_trace, PEquiv.mul_toMatrix_toPEquiv, Matrix.conjTranspose_intCast, Matrix.isUnit_diagonal, LinearEquiv.entryLinearMap_comp_mapMatrix, Matrix.submatrix_zero, matPolyEquiv_coeff_apply_aux_2, Matrix.rank_mul_le, Matrix.toLpLin_apply, Matrix.conjTranspose_smul_self, Matrix.entryLinearMap_toAddHom, Matrix.vec_mul_eq_mulVec, Matrix.toLin'_apply, Matrix.zpow_neg_natCast, Matrix.PosSemidef.inv, Matrix.conjTranspose_add, Matrix.GLPos.coe_neg_GL, Matrix.blockDiagonal'_tsum, Matrix.det_updateCol_smul_left, Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary, NumberField.Units.regulator_eq_det', LinearMap.BilinForm.SeparatingRight.toMatrix', Matrix.zero_zpow, Matrix.GeneralLinearGroup.coe_map_inv_mul_map, RingCon.matrix_apply, Matrix.mul_nonsing_inv, Matrix.isHermitian_intCast, ModularGroup.coe_S, LinearMap.toMatrix_adjoint, Matrix.vecMul_cons, Matrix.compLinearEquiv_apply, Matrix.exp_units_conj, EisensteinSeries.eisensteinSeries_slash_apply, LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, CongruenceSubgroup.IsCongruenceSubgroup.conjGL, Matrix.vecMul_intCast, LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero, Matrix.Module.smul_def', Matrix.zpow_neg_mul_zpow_self, LinearMap.BilinForm.Nondegenerate.toMatrix, RingEquiv.mapMatrix_trans, Matrix.permMatrix_refl, Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL, matPolyEquiv_smul_one, Matrix.l2_opNorm_def, Matrix.rank_unit, PEquiv.toMatrix_trans, Matrix.fromCols_inj, Matrix.inv_mulVec_eq_vec, LinearMap.toMatrixAlgEquiv_mul, Matrix.trace_mul_cycle', Matrix.replicateRow_smul, matrixEquivTensor_apply, Matrix.toEuclideanLin_toLp, Matrix.frobenius_nnnorm_transpose, MatrixEquivTensor.toFunAlgHom_apply, Matrix.mulVec_cons, Matrix.comp_symm_single, Matrix.head_transpose, Matrix.GeneralLinearGroup.injective_upperRightHom, Matrix.det_mul_right_comm, Matrix.entryLinearMap_toAddMonoidHom, Matrix.l2_opNorm_mul, Matrix.mul_diagonal, Matrix.fromCols_neg, Matrix.submatrix_mul, PEquiv.toMatrix_swap, Module.Basis.toMatrix_self, Matrix.vecMul_smul, Algebra.Norm.Transitivity.auxMat_toSquareBlock_eq, Matrix.scalar_commute_iff, LinearMap.det_toMatrix, Algebra.traceForm_toMatrix_powerBasis, Matrix.circulant_injective, Matrix.minpoly_toLin, basis_toMatrix_mul, Matrix.transvection_mul_apply_of_ne, instIsArtinianRingMatrix, Matrix.toLin'_toMatrix', Submodule.coe_matrix, Matrix.inv_subsingleton, LinearMap.det_toLin, CongruenceSubgroup.Gamma_mem, Matrix.PosDef.smul, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, LinearMap.posSemidef_toMatrix_iff, Matrix.smul_eq_diagonal_mul, Matrix.coe_ofLinearEquiv, ModularGroup.S_mul_S_eq, Matrix.kronecker_mulVec_vec_of_commute, Matrix.norm_replicateCol, LinearMap.mapMatrix_neg, Matrix.isIntegral, LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero', Matrix.mulVec.addMonoidHomLeft_apply, Matrix.SpecialLinearGroup.coe_mul, Matrix.Represents.algebraMap, Matrix.diagonal_intCast', Set.matrix_eq_pi, Matrix.adjugate_mul, Module.Basis.toMatrix_mul_toMatrix, matPolyEquiv_eq_X_pow_sub_C, Algebra.leftMulMatrix_eq_repr_mul, Matrix.UnitaryGroup.star_mul_self, ModularGroup.coeHom_apply, Matrix.self_mul_conjTranspose_eq_zero, LinearMap.SeparatingLeft.toMatrix₂', Matrix.subringCenter_eq_scalar_map, Matrix.derivative_det_one_add_X_smul_aux, MatrixModCat.toModuleCat_obj_isModule, Matrix.conjTranspose_mul, TensorProduct.toMatrix_comm, LinearMap.toMatrix₂'_apply, Matrix.aeval_eq_aeval_mod_charpoly, Subgroup.strictWidthInfty_SL2Z, Matrix.transpose_reindex, Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff, Matrix.inv_mul_cancel_left_of_invertible, Matrix.sub_scalar_sq_eq_discr, Matrix.kroneckerStarAlgEquiv_apply, Matrix.nnnorm_map_eq, Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂, Matrix.mul_adjp_add_detp, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, LinearMap.BilinForm.separatingLeft_toMatrix_iff, Matrix.zpow_sub, IsAzumaya.matrix, Matrix.SpecialLinearGroup.isInducing_toGL, Matrix.coe_ofAddEquiv, Matrix.mul_vecMulVec, Matrix.isSymm_transpose_mul_self, Real.volume_preserving_transvectionStruct, Matrix.zpow_add_one_of_ne_neg_one, Matrix.mul_swap_apply_right, Matrix.fromCols_mul_fromBlocks, Matrix.toLpLinAlgEquiv_symm_apply, Matrix.toBilin'_toMatrix', Matrix.reindex_updateCol, Matrix.uniformity, Matrix.Fin.circulant_mul, NumberField.Units.regOfFamily_eq_det', Matrix.toLinearMapₛₗ₂_toMatrix₂, Matrix.one_mulVec, Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials, Matrix.kroneckerMap_add_left, LinearMap.toMatrix'_mulVec, Matrix.diagonal_zero', Matrix.invOf_fromBlocks₁₁_eq, Matrix.SeparatingLeft.toLinearMap₂, Matrix.frobenius_norm_replicateRow, Matrix.isDiag_zero, Matrix.linfty_opNNNorm_diagonal, UpperHalfPlane.c_mul_im_sq_le_normSq_denom, hasEigenvector_toLin_diagonal, LinearMap.separatingRight_toLinearMap₂'_iff_det_ne_zero, dotProduct_toMatrix₂_mulVec, Matrix.entryLinearMap_eq_comp, Matrix.one_mul, Matrix.fromRows_inj, Matrix.diagonal_comp_single, Matrix.linfty_opNNNorm_def, Matrix.updateRow_zero_zero, Matrix.vecMul_zero, Subgroup.IsArithmetic.discreteTopology, LinearMap.toMatrixAlgEquiv_transpose_apply, UpperHalfPlane.smulAux'_im, Matrix.coe_units_zpow, Topology.IsClosedEmbedding.matrix_map, Matrix.fromCols_zero, Matrix.PosDef.posDef_sqrt, Matrix.conjTranspose_injective, RingCon.matrix_monotone, Matrix.piAlgEquiv_apply, Matrix.den_natCast, Matrix.isLeftRegular_iff_mulVec_injective, RootPairing.GeckConstruction.lie_e_f_mul_ω, LinearMap.traceAux_def, Matrix.kronecker_smul, Matrix.smul_mulVec, Algebra.leftMulMatrix_apply, Matrix.IsHermitian.star_eigenvectorUnitary_mulVec, InnerProductSpace.symm_toEuclideanLin_rankOne, LinearMap.BilinForm.toMatrix'_compRight, Matrix.inv_diagonal, IsSimpleRing.exists_algEquiv_matrix_divisionRing, Matrix.det_pow, Matrix.op_smul_eq_vecMul, Matrix.PosDef.mul_conjTranspose_self, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, Matrix.frobenius_nnnorm_conjTranspose, Matrix.conjTransposeAddEquiv_symm, Matrix.conjTranspose_ofNat, SymplecticGroup.J_mem, Matrix.kronecker_diagonal, Matrix.mvPolynomialX_mapMatrix_aeval, rank_matrix'', LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', Matrix.SeparatingRight.toBilin, Subgroup.IsArithmetic.conj, Matrix.rank_conjTranspose_mul_self, SlashInvariantForm.coe_norm, Matrix.adjugate_fin_two_of, Matrix.kroneckerMap_diagonal_left, Matrix.instNormedStarGroup, Matrix.algebraMap_matrix_apply, Matrix.blockTriangular_one, Matrix.transposeInvertibleEquivInvertible_apply, Matrix.transpose_eq_natCast, Matrix.transposeLinearEquiv_apply, Matrix.one_fin_two, LinearMap.toMatrix_apply, Matrix.BlockTriangular.mul, Matrix.isUnit_nonsing_inv_det, TwoSidedIdeal.matrix_strictMono_of_nonempty, Matrix.transpose_list_prod, Matrix.vecMul_surjective_iff_isUnit, Matrix.hadamard_one_eq_diagonal_iff, TensorProduct.toMatrix_map, Matrix.toLinAlgEquiv_toMatrixAlgEquiv, Matrix.rank_vecMulVec, Matrix.vec_bijective, Matrix.transpose_sum, Matrix.permanent_smul, Module.Basis.restrictScalars_toMatrix, Matrix.IsSymm.add, Matrix.piAddEquiv_apply, Matrix.center_eq_scalar_image, instContinuousSMulMatrix, Matrix.toLinAlgEquiv_symm, Algebra.Norm.Transitivity.det_mul_corner_pow, Matrix.IsHermitian.instContinuousFunctionalCalculus, LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrixAlgEquiv_transpose_apply', mulLinearMap_eq_mul, LinearMap.toMatrixRight'_comp, Matrix.frobenius_norm_transpose, Matrix.inv_inv_inv, Matrix.kroneckerStarAlgEquiv_symm_apply, IsOpen.matrix, Matrix.posSemidef_iff_isHermitian_and_spectrum_nonneg, Matrix.isPrimitive_iff, instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space, Matrix.trace_fin_two_of, Matrix.det_one_add_mul_comm, AddMonoidHom.mapMatrix_smul, Matrix.compAddEquiv_symm_apply, Matrix.mul_sum, QuadraticMap.toMatrix'_smul, Matrix.linfty_opNorm_def, Matrix.invOf_mul_cancel_left, summable_matrix_blockDiagonal, exists_mem_doublyStochastic_eq_smul_iff, Matrix.det_nonsing_inv, Matrix.algebraMap_eq_diagonalRingHom, LinearMap.mapMatrix_sub, Matrix.toBilin_comp, Matrix.blockDiagonal'_smul, Int.Matrix.exists_ne_zero_int_vec_norm_le, IsCusp.smul, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj, SimpleGraph.mem_ker_toLin'_lapMatrix_of_connectedComponent, Matrix.det_invOf, Matrix.SpecialLinearGroup.toGL_inj, Matrix.mul_transvection_apply_same, Matrix.toBlocks₂₁_diagonal, Matrix.IsDiag.sub, Matrix.compAddEquiv_apply, LinearMap.det_toMatrix_eq_det_toMatrix, Matrix.SpecialLinearGroup.toLin'_apply, MatrixModCat.fromMatrixLinear_apply_coe, Matrix.GeneralLinearGroup.toLin_apply, Matrix.mulVecLin_mul, Matrix.mulVec_injective_iff_isUnit, RingEquiv.mapMatrix_symm, Matrix.isNilpotent_iff_forall_col, Matrix.submatrix_neg, RootPairing.GeckConstruction.e_lie_u, Matrix.ext_addMonoidHom_iff, LinearMap.mapMatrixModule_comp_apply, Polynomial.coeff_det_X_add_C_zero, Matrix.norm_eq_sup_sup_nnnorm, Matrix.blockDiagonal_one, Matrix.linearIndependent_rows_iff_isUnit, RootPairing.GeckConstruction.lie_e_f_ne, Matrix.fromBlocks_diagonal_pow, Subgroup.hasDetPlusMinusOne_iff_abs_det, Matrix.PosSemidef.sqrt_eq_iff_eq_sq, Matrix.SpecialLinearGroup.mem_center_iff, Matrix.SpecialLinearGroup.isEmbedding_mapGL, Pi.basisFun_det_apply, Matrix.PosDef.inv, Matrix.Nondegenerate.toLinearMap₂', AlgHom.mulLeftRightMatrix.comp_inv, Matrix.mul_self_mul_conjTranspose_eq_zero, Matrix.det_comm, Matrix.submatrix_mem_matrix_iff, inner_matrix_col_col, Matrix.blockTriangular_reindex_iff, Matrix.isUnit_comp_symm_iff, Matrix.separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂, LieAlgebra.Orthogonal.pd_inv, Matrix.nnnorm_replicateCol, Matrix.inv_inv_of_invertible, LinearMap.toMatrixAlgEquiv'_comp, Matrix.mul_mul_apply, Matrix.TransvectionStruct.mul_inv, Matrix.one_div_zpow, Matrix.BlockTriangular.add_iff_left, Matrix.UnitaryGroup.inv_apply, PEquiv.single_mul_single, LinearMap.toMatrix₂Aux_apply, Matrix.SpecialLinearGroup.coe_mk, Matrix.conjTranspose_invOf, Matrix.diagonal_intCast, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, LieModule.toEnd_matrix, Matrix.det_smul_inv_vecMul_eq_cramer_transpose, Matrix.Fin.circulant_ite, ZLattice.covolume_eq_det, Matrix.charmatrix_zero, Matrix.mul_adjugate, Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans, Int.Matrix.exists_ne_zero_int_vec_norm_le', LinearMap.charpoly_toMatrix, LinearMap.toLinearMap₂'Aux_toMatrix₂Aux, Matrix.vecMulVec_sub, LinearMap.isSymm_iff_isHermitian_toMatrix, Matrix.replicateCol_add, Matrix.replicateRow_injective, ModularForm.slash_apply, Matrix.blockDiagonal'_pow, Matrix.kronecker_zero, Matrix.diag_sub, Matrix.toBilin'_single, Matrix.mulVec_mulVec, LinearMap.toMatrix_toLin, AlgEquiv.mapMatrix_apply, Matrix.zero_kroneckerTMul, LieAlgebra.SpecialLinear.sl_non_abelian, Matrix.GLPos.coe_neg, CongruenceSubgroup.Gamma0_mem, Matrix.mul_conjTranspose_mul_self_eq_zero, Matrix.conjTranspose_nsmul, Matrix.comp_one, Matrix.permMatrix_l2_opNorm_eq, SimpleGraph.incMatrix_mul_transpose_apply_of_adj, Matrix.conjTranspose_reindex, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, Matrix.toLinearEquiv_apply, hasEigenvalue_toLin_diagonal_iff, Matrix.vecMul_one, Matrix.GeneralLinearGroup.val_det_apply, UpperHalfPlane.petersson_slash, Matrix.spectrum_toLin', moritaEquivalenceMatrix_eqv, ModuleCat.toMatrixModCat_obj_isModule, Matrix.instIsDedekindFiniteMonoidOfIsStablyFiniteRing, Matrix.rank_self_mul_transpose, Matrix.GeneralLinearGroup.fin_two_smul_prod, kroneckerLinearEquiv_tmul

---

← Back to Index