Basic

📁 Source: Mathlib/Data/Matrix/Basic.lean

Statistics

Metric	Count
Definitions mapMatrix, mapMatrix, mapMatrix, mopMatrix, mapMatrix, mapMatrix, mapMatrix, mapMatrix, mapMatrixLinear, decidableEq, diagAddMonoidHom, diagLinearMap, diagonalAddMonoidHom, diagonalAlgHom, diagonalLinearMap, diagonalRingHom, entryAddHom, entryAddMonoidHom, entryLinearMap, instAlgebra, instFintypeOfDecidableEq, ofLinearEquiv, piAddEquiv, piAlgEquiv, piEquiv, piLinearEquiv, piRingEquiv, scalar, scalarAlgHom, transposeAddEquiv, transposeAlgEquiv, transposeLinearEquiv, transposeRingEquiv, mapMatrix, mopMatrix, mapMatrix	36
Theorems entryAddHom_comp_mapMatrix, mapMatrix_apply, mapMatrix_refl, mapMatrix_symm, mapMatrix_trans, entryAddMonoidHom_comp_mapMatrix, mapMatrix_add, mapMatrix_apply, mapMatrix_comp, mapMatrix_id, mapMatrix_neg, mapMatrix_smul, mapMatrix_sub, mapMatrix_zero, coe_matrix, coe_matrix, mapMatrix_apply, mapMatrix_refl, mapMatrix_symm, mapMatrix_trans, mopMatrix_apply, mopMatrix_symm_apply, mapMatrix_apply, mapMatrix_comp, mapMatrix_id, mapMatrix_apply, mapMatrix_refl, mapMatrix_symm, mapMatrix_trans, entryLinearMap_comp_mapMatrix, mapMatrix_apply, mapMatrix_refl, mapMatrix_symm, mapMatrix_toLinearMap, mapMatrix_trans, entryLinearMap_comp_mapMatrix, mapMatrixLinear_apply, mapMatrix_add, mapMatrix_apply, mapMatrix_comp, mapMatrix_id, mapMatrix_neg, mapMatrix_smul, mapMatrix_sub, mapMatrix_zero, algebraMap_eq_diagonal, algebraMap_eq_diagonalRingHom, algebraMap_matrix_apply, coe_ofLinearEquiv, coe_ofLinearEquiv_symm, diagAddMonoidHom_apply, diagLinearMap_apply, diag_list_sum, diag_multiset_sum, diag_sum, diagonalAddMonoidHom_apply, diagonalAlgHom_apply, diagonalLinearMap_apply, diagonalRingHom_apply, diagonal_pow, entryAddHom_apply, entryAddHom_eq_comp, entryAddMonoidHom_apply, entryAddMonoidHom_eq_comp, entryAddMonoidHom_toAddHom, entryLinearMap_apply, entryLinearMap_eq_comp, entryLinearMap_toAddHom, entryLinearMap_toAddMonoidHom, evalAddMonoidHom_comp_diagAddMonoidHom, instFinite, instIsStablyFiniteRingOfFinite, map_algebraMap, map_pow, mulVec_sum, piAddEquiv_apply, piAddEquiv_symm_apply, piAlgEquiv_apply, piAlgEquiv_symm_apply, piEquiv_apply, piEquiv_symm_apply, piLinearEquiv_apply, piLinearEquiv_symm_apply, piRingEquiv_apply, piRingEquiv_symm_apply, proj_comp_diagLinearMap, scalarAlgHom_apply, scalar_apply, scalar_comm, scalar_comm_iff, scalar_commute, scalar_commute_iff, scalar_inj, sum_apply, sum_mulVec, sum_vecMul, transposeAddEquiv_apply, transposeAddEquiv_symm, transposeAlgEquiv_apply, transposeAlgEquiv_symm_apply, transposeLinearEquiv_apply, transposeLinearEquiv_symm, transposeRingEquiv_apply, transposeRingEquiv_symm_apply, transpose_list_prod, transpose_list_sum, transpose_multiset_sum, transpose_pow, transpose_sum, vecMul_sum, zero_le_one_elem, zero_le_one_row, isStablyFiniteRing_iff, mapMatrix_apply, mapMatrix_refl, mapMatrix_symm, mapMatrix_trans, mopMatrix_apply, mopMatrix_symm_apply, mapMatrix_apply, mapMatrix_comp, mapMatrix_id, coe_matrix, coe_matrix, coe_matrix, instIsStablyFiniteRingMulOpposite	126
Total	162

AddEquiv

Definitions

Name	Category	Theorems
mapMatrix 📖	CompOp	5 math math: mapMatrix_trans, entryAddHom_comp_mapMatrix, mapMatrix_apply, mapMatrix_symm, mapMatrix_refl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
entryAddHom_comp_mapMatrix 📖	mathematical	—	AddHom.comp Matrix Matrix.add Matrix.entryAddHom AddHomClass.toAddHom AddEquiv EquivLike.toFunLike instEquivLike AddEquivClass.instAddHomClass instAddEquivClass mapMatrix	—	AddEquivClass.instAddHomClass instAddEquivClass
mapMatrix_apply 📖	mathematical	—	DFunLike.coe AddEquiv Matrix Matrix.add EquivLike.toFunLike instEquivLike mapMatrix Matrix.map	—	—
mapMatrix_refl 📖	mathematical	—	mapMatrix refl Matrix Matrix.add	—	—
mapMatrix_symm 📖	mathematical	—	symm Matrix Matrix.add mapMatrix	—	—
mapMatrix_trans 📖	mathematical	—	trans Matrix Matrix.add mapMatrix	—	—

AddMonoidHom

Definitions

Name	Category	Theorems
mapMatrix 📖	CompOp	9 math math: mapMatrix_comp, mapMatrix_id, mapMatrix_zero, entryAddMonoidHom_comp_mapMatrix, mapMatrix_sub, mapMatrix_neg, mapMatrix_apply, mapMatrix_add, mapMatrix_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
entryAddMonoidHom_comp_mapMatrix 📖	mathematical	—	comp Matrix AddZeroClass.toAddZero Matrix.addZeroClass Matrix.entryAddMonoidHom mapMatrix	—	—
mapMatrix_add 📖	mathematical	—	mapMatrix AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom AddZeroClass.toAddZero add Matrix Matrix.addZeroClass Matrix.addCommMonoid	—	—
mapMatrix_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Matrix AddZeroClass.toAddZero Matrix.addZeroClass instFunLike mapMatrix Matrix.map	—	—
mapMatrix_comp 📖	mathematical	—	comp Matrix AddZeroClass.toAddZero Matrix.addZeroClass mapMatrix	—	—
mapMatrix_id 📖	mathematical	—	mapMatrix id AddZeroClass.toAddZero Matrix Matrix.addZeroClass	—	—
mapMatrix_neg 📖	mathematical	—	mapMatrix AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom AddZeroClass.toAddZero instNeg Matrix Matrix.addZeroClass Matrix.addCommGroup	—	—
mapMatrix_smul 📖	mathematical	—	mapMatrix AddMonoid.toAddZeroClass AddMonoidHom AddZeroClass.toAddZero SMulZeroClass.toSMul instZeroAddMonoidHom instSMulZeroClassOfDistribSMul DistribMulAction.toDistribSMul Matrix Matrix.addZeroClass Matrix.addMonoid Matrix.distribMulAction	—	—
mapMatrix_sub 📖	mathematical	—	mapMatrix AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom AddZeroClass.toAddZero instSub Matrix Matrix.addZeroClass Matrix.addCommGroup	—	—
mapMatrix_zero 📖	mathematical	—	mapMatrix AddMonoidHom AddZeroClass.toAddZero instZeroAddMonoidHom Matrix Matrix.addZeroClass	—	—

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_matrix 📖	mathematical	—	SetLike.coe AddSubgroup Matrix Matrix.addGroup instSetLike matrix Set.matrix	—	—

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_matrix 📖	mathematical	—	SetLike.coe AddSubmonoid Matrix Matrix.addZeroClass AddMonoid.toAddZeroClass instSetLike matrix Set.matrix	—	—

AlgEquiv

Definitions

Name	Category	Theorems
mapMatrix 📖	CompOp	5 math math: mapMatrix_refl, mapMatrix_symm, map_det, mapMatrix_trans, mapMatrix_apply
mopMatrix 📖	CompOp	2 math math: mopMatrix_apply, mopMatrix_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMatrix_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix Matrix.semiring Matrix.instAlgebra instFunLike mapMatrix Matrix.map	—	—
mapMatrix_refl 📖	mathematical	—	mapMatrix refl Matrix Matrix.semiring Matrix.instAlgebra	—	—
mapMatrix_symm 📖	mathematical	—	symm Matrix Matrix.semiring Matrix.instAlgebra mapMatrix	—	—
mapMatrix_trans 📖	mathematical	—	trans Matrix Matrix.semiring Matrix.instAlgebra mapMatrix	—	—
mopMatrix_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix MulOpposite Matrix.semiring MulOpposite.instSemiring Matrix.instAlgebra MulOpposite.instAlgebra instFunLike mopMatrix MulOpposite.op Matrix.map Matrix.transpose MulOpposite.unop	—	—
mopMatrix_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MulOpposite Matrix MulOpposite.instSemiring Matrix.semiring MulOpposite.instAlgebra Matrix.instAlgebra instFunLike symm mopMatrix Matrix.map Matrix.transpose MulOpposite.unop MulOpposite.op	—	—

AlgHom

Definitions

Name	Category	Theorems
mapMatrix 📖	CompOp	7 math math: Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, map_adjugate, map_det, mapMatrix_apply, mapMatrix_comp, mapMatrix_id, Matrix.mvPolynomialX_mapMatrix_aeval

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMatrix_apply 📖	mathematical	—	DFunLike.coe AlgHom Matrix Matrix.semiring Matrix.instAlgebra funLike mapMatrix Matrix.map	—	—
mapMatrix_comp 📖	mathematical	—	comp Matrix Matrix.semiring Matrix.instAlgebra mapMatrix	—	—
mapMatrix_id 📖	mathematical	—	mapMatrix id Matrix Matrix.semiring Matrix.instAlgebra	—	—

Equiv

Definitions

Name	Category	Theorems
mapMatrix 📖	CompOp	5 math math: mapMatrix_symm, mapMatrix_apply, mapMatrix_trans, Matrix.kroneckerMap_assoc, mapMatrix_refl

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMatrix_apply 📖	mathematical	—	DFunLike.coe Equiv Matrix EquivLike.toFunLike instEquivLike mapMatrix Matrix.map	—	—
mapMatrix_refl 📖	mathematical	—	mapMatrix refl Matrix	—	—
mapMatrix_symm 📖	mathematical	—	symm Matrix mapMatrix	—	—
mapMatrix_trans 📖	mathematical	—	trans Matrix mapMatrix	—	—

LinearEquiv

Definitions

Name	Category	Theorems
mapMatrix 📖	CompOp	6 math math: mapMatrix_apply, mapMatrix_toLinearMap, mapMatrix_symm, mapMatrix_refl, mapMatrix_trans, entryLinearMap_comp_mapMatrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
entryLinearMap_comp_mapMatrix 📖	mathematical	—	LinearMap.comp Matrix Matrix.addCommMonoid Matrix.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.right_ids Matrix.entryLinearMap toLinearMap mapMatrix RingHomCompTriple.ids	—	RingHomCompTriple.right_ids RingHomCompTriple.ids LinearMap.comp.congr_simp mapMatrix_toLinearMap
mapMatrix_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Matrix Matrix.addCommMonoid Matrix.module EquivLike.toFunLike instEquivLike mapMatrix Matrix.map	—	—
mapMatrix_refl 📖	mathematical	—	mapMatrix RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids refl Matrix Matrix.addCommMonoid Matrix.module	—	RingHomInvPair.ids
mapMatrix_symm 📖	mathematical	—	symm Matrix Matrix.addCommMonoid Matrix.module mapMatrix	—	—
mapMatrix_toLinearMap 📖	mathematical	—	toLinearMap Matrix Matrix.addCommMonoid Matrix.module mapMatrix LinearMap.mapMatrix	—	—
mapMatrix_trans 📖	mathematical	—	trans Matrix Matrix.addCommMonoid Matrix.module mapMatrix	—	—

LinearMap

Definitions

Name	Category	Theorems
mapMatrix 📖	CompOp	11 math math: mapMatrix_zero, mapMatrixLinear_apply, entryLinearMap_comp_mapMatrix, LinearEquiv.mapMatrix_toLinearMap, mapMatrix_smul, mapMatrix_comp, mapMatrix_apply, mapMatrix_id, mapMatrix_add, mapMatrix_neg, mapMatrix_sub
mapMatrixLinear 📖	CompOp	1 math math: mapMatrixLinear_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
entryLinearMap_comp_mapMatrix 📖	mathematical	—	comp Matrix Matrix.addCommMonoid Matrix.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.right_ids Matrix.entryLinearMap mapMatrix RingHomCompTriple.ids	—	RingHomCompTriple.right_ids
mapMatrixLinear_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Matrix Matrix.addCommMonoid Matrix.module addCommMonoid module Matrix.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike mapMatrixLinear mapMatrix	—	Matrix.smulCommClass
mapMatrix_add 📖	mathematical	—	mapMatrix LinearMap instAdd Matrix Matrix.addCommMonoid Matrix.module	—	—
mapMatrix_apply 📖	mathematical	—	DFunLike.coe LinearMap Matrix Matrix.addCommMonoid Matrix.module instFunLike mapMatrix Matrix.map	—	—
mapMatrix_comp 📖	mathematical	—	comp Matrix Matrix.addCommMonoid Matrix.module mapMatrix	—	—
mapMatrix_id 📖	mathematical	—	mapMatrix RingHom.id Semiring.toNonAssocSemiring id Matrix Matrix.addCommMonoid Matrix.module	—	—
mapMatrix_neg 📖	mathematical	—	mapMatrix AddCommGroup.toAddCommMonoid LinearMap instNeg Matrix Matrix.addCommMonoid Matrix.module Matrix.addCommGroup	—	—
mapMatrix_smul 📖	mathematical	—	mapMatrix LinearMap instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid Matrix Matrix.addCommMonoid Matrix.module Matrix.distribMulAction Matrix.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction Module.toDistribMulAction	—	—
mapMatrix_sub 📖	mathematical	—	mapMatrix AddCommGroup.toAddCommMonoid LinearMap instSub Matrix Matrix.addCommMonoid Matrix.module Matrix.addCommGroup	—	—
mapMatrix_zero 📖	mathematical	—	mapMatrix LinearMap instZero Matrix Matrix.addCommMonoid Matrix.module	—	—

Matrix

Definitions

Name	Category	Theorems
decidableEq 📖	CompOp	—
diagAddMonoidHom 📖	CompOp	3 math math: diagLinearMap_apply, evalAddMonoidHom_comp_diagAddMonoidHom, diagAddMonoidHom_apply
diagLinearMap 📖	CompOp	2 math math: diagLinearMap_apply, proj_comp_diagLinearMap
diagonalAddMonoidHom 📖	CompOp	2 math math: diagonalLinearMap_apply, diagonalAddMonoidHom_apply
diagonalAlgHom 📖	CompOp	1 math math: diagonalAlgHom_apply
diagonalLinearMap 📖	CompOp	2 math math: diagonalLinearMap_apply, RootPairing.GeckConstruction.span_range_h_le_range_diagonal
diagonalRingHom 📖	CompOp	2 math math: diagonalRingHom_apply, algebraMap_eq_diagonalRingHom
entryAddHom 📖	CompOp	5 math math: entryAddHom_apply, entryAddHom_eq_comp, AddEquiv.entryAddHom_comp_mapMatrix, entryAddMonoidHom_toAddHom, entryLinearMap_toAddHom
entryAddMonoidHom 📖	CompOp	6 math math: entryAddMonoidHom_eq_comp, AddMonoidHom.entryAddMonoidHom_comp_mapMatrix, entryAddMonoidHom_apply, evalAddMonoidHom_comp_diagAddMonoidHom, entryAddMonoidHom_toAddHom, entryLinearMap_toAddMonoidHom
entryLinearMap 📖	CompOp	7 math math: LinearMap.entryLinearMap_comp_mapMatrix, proj_comp_diagLinearMap, entryLinearMap_apply, LinearEquiv.entryLinearMap_comp_mapMatrix, entryLinearMap_toAddHom, entryLinearMap_toAddMonoidHom, entryLinearMap_eq_comp
instAlgebra 📖	CompOp	235 math math: LinearMap.restrictScalars_toMatrix, toLinAlgEquiv_one, Algebra.IsCentral.matrix, LinearMap.toMatrixAlgEquiv'_mul, kroneckerTMulStarAlgEquiv_symm_apply, IsHermitian.isClosedEmbedding_cfcAux, pow_eq_aeval_mod_charpoly, IsHermitian.det_abs, RootPairing.GeckConstruction.instHasTrivialRadical, compAlgEquiv_apply, spectrum_toEuclideanLin, LieAlgebra.Orthogonal.mem_so, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, IsHermitian.cfc_eq, IsMoritaEquivalent.matrix, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, lieConj_apply, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, LinearMap.toMatrixAlgEquiv_comp, Algebra.norm_eq_matrix_det, spectrum_toLpLin, LieModule.instIsFaithfulMatrixForall, PosSemidef.sqrt_eq_zero_iff, mem_spectrum_iff_isRoot_charpoly, Algebra.smul_leftMulMatrix, LinearMap.toMatrixAlgEquiv_toLinAlgEquiv, Algebra.map_leftMulMatrix_localization, matPolyEquiv_map_smul, Module.Basis.toMatrix_smul, LinearMap.spectrum_toMatrix', matPolyEquiv_diagonal_X, AlgHom.mulLeftRightMatrix.inv_comp, spectrum_diagonal, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, Algebra.toMatrix_lmul_eq, LinearMap.toMatrixAlgEquiv'_id, LieAlgebra.SpecialLinear.singleSubSingle_add_singleSubSingle, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, minpoly_dvd_charpoly, LinearMap.toMatrixAlgEquiv_apply, toAlgEquiv_kroneckerStarAlgEquiv, LieAlgebra.Orthogonal.indefiniteDiagonal_assoc, toLinAlgEquiv_mul, PosSemidef.det_sqrt, toAlgEquiv_kroneckerTMulStarAlgEquiv, matPolyEquiv_coeff_apply_aux_1, Algebra.leftMulMatrix_injective, mem_spectrum_of_isRoot_charpoly, IsHermitian.charpoly_cfc_eq, LinearMap.detAux_def, matPolyEquiv_symm_apply_coeff, LinearMap.toMatrixAlgEquiv_id, PowerBasis.leftMulMatrix, PosSemidef.posSemidef_sqrt, finite_spectrum, AlgEquiv.mopMatrix_apply, isRepresentation.toEnd_represents, det_reindexAlgEquiv, PosSemidef.sqrt_eq_one_iff, PosSemidef.sqrt_sq, charpoly_leftMulMatrix, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, lieEquivMatrix'_apply, LinearMap.minpoly_toMatrix', PosSemidef.eq_sqrt_iff_sq_eq, instFiniteSpectrum, AlgHom.map_adjugate, TransvectionStruct.toMatrix_reindexEquiv_prod, AlgEquiv.mapMatrix_refl, kroneckerAlgEquiv_apply, map_algebraMap, RootPairing.GeckConstruction.trace_toEnd_eq_zero, instLieModuleForall, TransvectionStruct.toMatrix_reindexEquiv, AlgHom.map_det, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, LinearMap.toMatrixAlgEquiv'_apply, AlgHom.mapMatrix_apply, RootPairing.GeckConstruction.span_range_h'_eq_top, uniqueAlgEquiv_apply, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing, isRepresentation.toEnd_exists_mem_ideal, reindexAlgEquiv_mul, AlgHom.mapMatrix_comp, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', reindexLieEquiv_apply, IsHermitian.cfcAux_apply, LieAlgebra.SpecialLinear.sl_bracket, kroneckerTMulAlgEquiv_symm_apply, kroneckerTMulStarAlgEquiv_apply, AlgEquiv.mapMatrix_symm, reindexLieEquiv_symm, instFiniteElemRealSpectrum, scalarAlgHom_apply, mem_skewAdjointMatricesLieSubalgebra, lieConj_symm_apply, kroneckerTMulLinearEquiv_mul, IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite, dualNumberEquiv_symm_apply, matPolyEquiv_charmatrix, RootPairing.GeckConstruction.instIsIrreducible, LinearMap.spectrum_toMatrix, Subalgebra.coe_matrix, toLinAlgEquiv'_apply, minpoly_toLin', Algebra.smulTower_leftMulMatrix, LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv', RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, algebraMap_eq_diagonal, PosSemidef.isUnit_sqrt_iff, reindexAlgEquiv_symm, IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed, LinearMap.toMatrixAlgEquiv_symm, IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite, LinearMap.minpoly_toMatrix, matrixEquivTensor_apply_single, matPolyEquiv_map_C, Algebra.leftMulMatrix_complex, IsHermitian.spectrum_eq_image_range, MatrixEquivTensor.invFun_smul, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, matrixEquivTensor_apply_symm, MatrixEquivTensor.left_inv, Algebra.smulTower_leftMulMatrix_algebraMap_ne, eval_det, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, IsHermitian.spectral_theorem, diagonalAlgHom_apply, PosSemidef.sq_sqrt, RootPairing.GeckConstruction.ωConj_invFun, endVecAlgEquivMatrixEnd_apply_apply, AlgHom.mapMatrix_id, Algebra.trace_eq_matrix_trace, matPolyEquiv_symm_C, spectrum_toLin, PosSemidef.inv_sqrt, compAlgEquiv_symm_apply, finite_real_spectrum, mem_skewAdjointMatricesLieSubalgebra_unit_smul, IsSemisimpleModule.exists_end_algEquiv, toLpLinAlgEquiv_apply_apply_ofLp, toLinAlgEquiv_apply, Algebra.smulTower_leftMulMatrix_algebraMap, RootPairing.GeckConstruction.ωConj_toFun, LieAlgebra.SpecialLinear.val_single, reindexAlgEquiv_refl, lieEquivMatrix'_symm_apply, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle, matPolyEquiv_eval_eq_map, RootPairing.GeckConstruction.h_mem_lieAlgebra, matPolyEquiv_coeff_apply, piAlgEquiv_symm_apply, IsHermitian.spectrum_real_eq_range_eigenvalues, isRepresentation.toEnd_surjective, toLinAlgEquiv_self, kroneckerAlgEquiv_symm_apply, IsHermitian.cfcAux_id, AlgEquiv.map_det, LinearMap.toMatrixAlgEquiv'_symm, uniqueAlgEquiv_symm_apply, transposeAlgEquiv_apply, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, subalgebraCenter_eq_scalarAlgHom_map, reindexAlgEquiv_apply, Algebra.leftMulMatrix_mulVec_repr, dualNumberEquiv_apply, support_subset_support_matPolyEquiv, toLinAlgEquiv'_toMatrixAlgEquiv', kroneckerTMulAlgEquiv_apply, matPolyEquiv_symm_map_eval, endVecAlgEquivMatrixEnd_symm_apply_apply, IsHermitian.eigenvalues_mem_spectrum_real, AlgEquiv.mapMatrix_trans, toLinAlgEquiv'_one, MatrixEquivTensor.right_inv, matPolyEquiv_eval, AlgEquiv.mopMatrix_symm_apply, transposeAlgEquiv_symm_apply, toLinAlgEquiv'_symm, toLinearEquiv_kroneckerAlgEquiv, IsHermitian.star_mul_self_mul_eq_diagonal, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite, IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed, matPolyEquiv_symm_X, aeval_self_charpoly, Module.Basis.toMatrix_reindex', LinearMap.toMatrixAlgEquiv_apply', PosSemidef.sqrt_mul_self, RootPairing.GeckConstruction.f_mem_lieAlgebra, RootPairing.GeckConstruction.e_mem_lieAlgebra, LieAlgebra.SpecialLinear.val_singleSubSingle, Algebra.smulTower_leftMulMatrix_algebraMap_eq, skewAdjointMatricesLieSubalgebraEquiv_apply, LinearMap.toMatrixAlgEquiv_reindexRange, Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, matPolyEquiv_coeff_apply_aux_2, IsHermitian.conjStarAlgAut_star_eigenvectorUnitary, matPolyEquiv_smul_one, LinearMap.toMatrixAlgEquiv_mul, matrixEquivTensor_apply, MatrixEquivTensor.toFunAlgHom_apply, minpoly_toLin, isIntegral, Represents.algebraMap, matPolyEquiv_eq_X_pow_sub_C, Algebra.leftMulMatrix_eq_repr_mul, aeval_eq_aeval_mod_charpoly, kroneckerStarAlgEquiv_apply, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, IsAzumaya.matrix, toLpLinAlgEquiv_symm_apply, LinearMap.toMatrixAlgEquiv_transpose_apply, PosDef.posDef_sqrt, piAlgEquiv_apply, Algebra.leftMulMatrix_apply, IsSimpleRing.exists_algEquiv_matrix_divisionRing, mvPolynomialX_mapMatrix_aeval, LieAlgebra.SpecialLinear.singleSubSingle_sub_singleSubSingle', algebraMap_matrix_apply, toLinAlgEquiv_toMatrixAlgEquiv, toLinAlgEquiv_symm, IsHermitian.instContinuousFunctionalCalculus, LinearMap.toMatrixAlgEquiv_transpose_apply', kroneckerStarAlgEquiv_symm_apply, posSemidef_iff_isHermitian_and_spectrum_nonneg, algebraMap_eq_diagonalRingHom, PosSemidef.sqrt_eq_iff_eq_sq, AlgHom.mulLeftRightMatrix.comp_inv, LinearMap.toMatrixAlgEquiv'_comp, LieModule.toEnd_matrix, AlgEquiv.mapMatrix_apply, LieAlgebra.SpecialLinear.sl_non_abelian, spectrum_toLin', moritaEquivalenceMatrix_eqv
instFintypeOfDecidableEq 📖	CompOp	—
ofLinearEquiv 📖	CompOp	3 math math: coe_ofLinearEquiv_symm, coe_ofLinearEquiv, entryLinearMap_eq_comp
piAddEquiv 📖	CompOp	4 math math: piLinearEquiv_apply, piAddEquiv_symm_apply, piLinearEquiv_symm_apply, piAddEquiv_apply
piAlgEquiv 📖	CompOp	2 math math: piAlgEquiv_symm_apply, piAlgEquiv_apply
piEquiv 📖	CompOp	2 math math: piEquiv_symm_apply, piEquiv_apply
piLinearEquiv 📖	CompOp	2 math math: piLinearEquiv_apply, piLinearEquiv_symm_apply
piRingEquiv 📖	CompOp	2 math math: piRingEquiv_apply, piRingEquiv_symm_apply
scalar 📖	CompOp	42 math math: scalar_inj, scalar_comm, isParabolic_iff_exists, GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, SpecialLinearGroup.scalar_eq_self_of_mem_center, mem_range_scalar_iff_commute_transvectionStruct, center_eq_range, IsParabolic.sub_eigenvalue_sq_eq_zero, charpoly_sub_scalar, toLin_scalar, subsemiringCenter_eq_scalar_map, GeneralLinearGroup.fixpointPolynomial_eq_zero_iff, LinearMap.toMatrix'_algebraMap, mem_range_scalar_iff_commute_single, SpecialLinearGroup.scalar_eq_coe_self_center, scalar_commute, scalarAlgHom_apply, LinearMap.toMatrix_algebraMap, Module.scalar_smul, submonoidCenter_eq_scalar_map, mem_range_scalar_iff_commute_single', sub_scalar_sq_eq_disc, subsemigroupCenter_eq_scalar_map, eval_det, GeneralLinearGroup.mem_center_iff_val_eq_scalar, mem_range_scalar_of_commute_single, scalar_comm_iff, MatrixModCat.isScalarTower_toModuleCat, eval_charpoly, SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, matPolyEquiv_eval_eq_map, circulant_single, matPolyEquiv_symm_map_eval, matPolyEquiv_eval, scalar_apply, mem_range_scalar_of_commute_transvectionStruct, scalar_commute_iff, subringCenter_eq_scalar_map, sub_scalar_sq_eq_discr, center_eq_scalar_image, SpecialLinearGroup.mem_center_iff, charmatrix_zero
scalarAlgHom 📖	CompOp	2 math math: scalarAlgHom_apply, subalgebraCenter_eq_scalarAlgHom_map
transposeAddEquiv 📖	CompOp	4 math math: transposeAddEquiv_symm, transposeAddEquiv_apply, transposeAlgEquiv_symm_apply, transposeLinearEquiv_apply
transposeAlgEquiv 📖	CompOp	2 math math: transposeAlgEquiv_apply, transposeAlgEquiv_symm_apply
transposeLinearEquiv 📖	CompOp	2 math math: transposeLinearEquiv_symm, transposeLinearEquiv_apply
transposeRingEquiv 📖	CompOp	2 math math: transposeRingEquiv_symm_apply, transposeRingEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_eq_diagonal 📖	mathematical	—	DFunLike.coe RingHom Matrix Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring RingHom.instFunLike algebraMap instAlgebra diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.semiring Function.algebra	—	—
algebraMap_eq_diagonalRingHom 📖	mathematical	—	algebraMap Matrix semiring instAlgebra RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.nonAssocSemiring nonAssocSemiring diagonalRingHom Pi.semiring Function.algebra	—	—
algebraMap_matrix_apply 📖	mathematical	—	DFunLike.coe RingHom Matrix Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring RingHom.instFunLike algebraMap instAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
coe_ofLinearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix Pi.addCommMonoid addCommMonoid Pi.Function.module module EquivLike.toFunLike LinearEquiv.instEquivLike ofLinearEquiv Equiv Equiv.instEquivLike of	—	RingHomInvPair.ids
coe_ofLinearEquiv_symm 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix addCommMonoid Pi.addCommMonoid module Pi.Function.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm ofLinearEquiv Equiv Equiv.instEquivLike Equiv.symm of	—	RingHomInvPair.ids
diagAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Matrix AddZeroClass.toAddZero addZeroClass Pi.addZeroClass AddMonoidHom.instFunLike diagAddMonoidHom diag	—	—
diagLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Matrix addCommMonoid Pi.addCommMonoid module Pi.Function.module LinearMap.instFunLike diagLinearMap ZeroHom.toFun AddZero.toZero AddZeroClass.toAddZero addZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addZeroClass AddMonoidHom.toZeroHom diagAddMonoidHom	—	—
diag_list_sum 📖	mathematical	—	diag Matrix add AddSemigroup.toAdd AddMonoid.toAddSemigroup zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Pi.instAdd Pi.instZero	—	map_list_sum AddMonoidHom.instAddMonoidHomClass
diag_multiset_sum 📖	mathematical	—	diag Multiset.sum Matrix addCommMonoid Pi.addCommMonoid Multiset.map	—	map_multiset_sum AddMonoidHom.instAddMonoidHomClass
diag_sum 📖	mathematical	—	diag Finset.sum Matrix addCommMonoid Pi.addCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
diagonalAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Matrix AddZeroClass.toAddZero Pi.addZeroClass addZeroClass AddMonoidHom.instFunLike diagonalAddMonoidHom diagonal AddZero.toZero	—	—
diagonalAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom Matrix Pi.semiring semiring Function.algebra instAlgebra AlgHom.funLike diagonalAlgHom diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
diagonalLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Matrix Pi.addCommMonoid addCommMonoid Pi.Function.module module LinearMap.instFunLike diagonalLinearMap ZeroHom.toFun AddZero.toZero AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addZeroClass AddMonoidHom.toZeroHom diagonalAddMonoidHom	—	—
diagonalRingHom_apply 📖	mathematical	—	DFunLike.coe RingHom Matrix Pi.nonAssocSemiring nonAssocSemiring RingHom.instFunLike diagonalRingHom diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
diagonal_pow 📖	mathematical	—	Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.instPow	—	map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
entryAddHom_apply 📖	mathematical	—	DFunLike.coe AddHom Matrix add AddHom.funLike entryAddHom	—	—
entryAddHom_eq_comp 📖	mathematical	—	entryAddHom AddHom.comp Matrix add Pi.instAdd Pi.evalAddHom AddHomClass.toAddHom AddEquiv EquivLike.toFunLike AddEquiv.instEquivLike AddEquivClass.instAddHomClass AddEquiv.instAddEquivClass AddEquiv.symm ofAddEquiv	—	—
entryAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Matrix AddZeroClass.toAddZero addZeroClass AddMonoidHom.instFunLike entryAddMonoidHom	—	—
entryAddMonoidHom_eq_comp 📖	mathematical	—	entryAddMonoidHom AddMonoidHom.comp Matrix AddZeroClass.toAddZero addZeroClass Pi.addZeroClass Pi.evalAddMonoidHom AddMonoidHomClass.toAddMonoidHom AddEquiv add AddZero.toAdd Pi.instAdd EquivLike.toFunLike AddEquiv.instEquivLike AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass AddEquiv.symm ofAddEquiv	—	—
entryAddMonoidHom_toAddHom 📖	mathematical	—	AddHomClass.toAddHom Matrix AddMonoidHom AddZeroClass.toAddZero addZeroClass add AddZero.toAdd AddMonoidHom.instFunLike AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass entryAddMonoidHom entryAddHom	—	AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
entryLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Matrix addCommMonoid module LinearMap.instFunLike entryLinearMap	—	—
entryLinearMap_eq_comp 📖	mathematical	—	entryLinearMap LinearMap.comp Matrix addCommMonoid Pi.addCommMonoid module Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.proj Pi.Function.module LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm ofLinearEquiv	—	—
entryLinearMap_toAddHom 📖	mathematical	—	AddHomClass.toAddHom Matrix LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid module add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.instFunLike SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass entryLinearMap entryAddHom	—	SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass
entryLinearMap_toAddMonoidHom 📖	mathematical	—	AddMonoidHomClass.toAddMonoidHom Matrix LinearMap RingHom.id Semiring.toNonAssocSemiring addCommMonoid module AddZeroClass.toAddZero addZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearMap.instFunLike DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero addMonoid Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass entryLinearMap entryAddMonoidHom	—	DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
evalAddMonoidHom_comp_diagAddMonoidHom 📖	mathematical	—	AddMonoidHom.comp Matrix AddZeroClass.toAddZero addZeroClass Pi.addZeroClass Pi.evalAddMonoidHom diagAddMonoidHom entryAddMonoidHom	—	—
instFinite 📖	mathematical	—	Finite Matrix	—	Pi.finite
instIsStablyFiniteRingOfFinite 📖	mathematical	—	IsStablyFiniteRing MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring	—	instIsDedekindFiniteMonoidOfFinite instFinite Finite.of_fintype
map_algebraMap 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	map Matrix semiring instAlgebra	—	algebraMap_eq_diagonal diagonal_map
map_pow 📖	mathematical	—	map Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	RingHom.map_pow
mulVec_sum 📖	mathematical	—	mulVec Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	dotProduct_sum Finset.sum_apply Finset.sum_congr
piAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv Matrix add Pi.instAdd EquivLike.toFunLike AddEquiv.instEquivLike piAddEquiv map	—	—
piAddEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv Matrix Pi.instAdd add EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm piAddEquiv Equiv Equiv.instEquivLike of	—	—
piAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix semiring Pi.semiring instAlgebra Pi.algebra AlgEquiv.instFunLike piAlgEquiv map	—	—
piAlgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix Pi.semiring semiring Pi.algebra instAlgebra AlgEquiv.instFunLike AlgEquiv.symm piAlgEquiv Equiv EquivLike.toFunLike Equiv.instEquivLike of	—	—
piEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike piEquiv map	—	—
piEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Equiv.symm piEquiv of	—	—
piLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix addCommMonoid Pi.addCommMonoid module Pi.module EquivLike.toFunLike LinearEquiv.instEquivLike piLinearEquiv Equiv.toFun AddEquiv.toEquiv add Pi.instAdd AddSemigroup.toAdd piAddEquiv	—	RingHomInvPair.ids
piLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix Pi.addCommMonoid addCommMonoid Pi.module module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm piLinearEquiv Equiv.invFun AddEquiv.toEquiv add Pi.instAdd AddSemigroup.toAdd piAddEquiv	—	RingHomInvPair.ids
piRingEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv Matrix instMulOfFintypeOfAddCommMonoid Pi.instMul Pi.addCommMonoid add Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike RingEquiv.instEquivLike piRingEquiv map	—	—
piRingEquiv_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Matrix Pi.instMul instMulOfFintypeOfAddCommMonoid Pi.addCommMonoid Pi.instAdd add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm piRingEquiv Equiv Equiv.instEquivLike of	—	—
proj_comp_diagLinearMap 📖	mathematical	—	LinearMap.comp Matrix addCommMonoid Pi.addCommMonoid module Pi.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.proj diagLinearMap entryLinearMap	—	RingHomCompTriple.ids
scalarAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom Matrix semiring instAlgebra AlgHom.funLike scalarAlgHom RingHom Semiring.toNonAssocSemiring nonAssocSemiring RingHom.instFunLike scalar	—	—
scalar_apply 📖	mathematical	—	DFunLike.coe RingHom Matrix Semiring.toNonAssocSemiring nonAssocSemiring RingHom.instFunLike scalar diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
scalar_comm 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Matrix instHMulOfFintypeOfMulOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe RingHom nonAssocSemiring RingHom.instFunLike scalar	—	scalar_comm_iff ext
scalar_comm_iff 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe RingHom nonAssocSemiring RingHom.instFunLike scalar smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul MulOpposite DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule MulOpposite.op	—	—
scalar_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Matrix instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe RingHom nonAssocSemiring RingHom.instFunLike scalar	—	scalar_comm
scalar_commute_iff 📖	mathematical	—	Commute Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe RingHom nonAssocSemiring RingHom.instFunLike scalar smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul MulOpposite DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulOpposite.instSemiring Semiring.toOppositeModule MulOpposite.op	—	scalar_comm_iff
scalar_inj 📖	mathematical	—	DFunLike.coe RingHom Matrix Semiring.toNonAssocSemiring nonAssocSemiring RingHom.instFunLike scalar	—	diagonal_injective Function.const_injective
sum_apply 📖	mathematical	—	Finset.sum Matrix addCommMonoid	—	Finset.sum_apply
sum_mulVec 📖	mathematical	—	mulVec Finset.sum Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.addCommMonoid	—	Finset.sum_congr sum_apply Finset.sum_mul Finset.sum_apply Finset.sum_comm
sum_vecMul 📖	mathematical	—	vecMul Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	sum_dotProduct Finset.sum_apply Finset.sum_congr
transposeAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv Matrix add EquivLike.toFunLike AddEquiv.instEquivLike transposeAddEquiv transpose	—	—
transposeAddEquiv_symm 📖	mathematical	—	AddEquiv.symm Matrix add transposeAddEquiv	—	—
transposeAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix MulOpposite semiring CommSemiring.toSemiring MulOpposite.instSemiring instAlgebra MulOpposite.instAlgebra AlgEquiv.instFunLike transposeAlgEquiv MulOpposite.op transpose	—	—
transposeAlgEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv MulOpposite Matrix MulOpposite.instSemiring semiring CommSemiring.toSemiring MulOpposite.instAlgebra instAlgebra AlgEquiv.instFunLike AlgEquiv.symm transposeAlgEquiv Equiv.invFun AddEquiv.toEquiv add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instAdd AddEquiv.trans transposeAddEquiv MulOpposite.opAddEquiv	—	—
transposeLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix addCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike transposeLinearEquiv Equiv.toFun AddEquiv.toEquiv add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup transposeAddEquiv	—	RingHomInvPair.ids
transposeLinearEquiv_symm 📖	mathematical	—	LinearEquiv.symm Matrix addCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids transposeLinearEquiv	—	RingHomInvPair.ids
transposeRingEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv Matrix MulOpposite instMulOfFintypeOfAddCommMonoid CommMagma.toMul CommSemigroup.toCommMagma MulOpposite.instMul add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup MulOpposite.instAdd EquivLike.toFunLike RingEquiv.instEquivLike transposeRingEquiv MulOpposite.op transpose	—	—
transposeRingEquiv_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite Matrix MulOpposite.instMul instMulOfFintypeOfAddCommMonoid CommMagma.toMul CommSemigroup.toCommMagma MulOpposite.instAdd add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm transposeRingEquiv transpose MulOpposite.unop	—	—
transpose_list_prod 📖	mathematical	—	transpose Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingEquiv.unop_map_list_prod
transpose_list_sum 📖	mathematical	—	transpose Matrix add AddSemigroup.toAdd AddMonoid.toAddSemigroup zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	map_list_sum AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
transpose_multiset_sum 📖	mathematical	—	transpose Multiset.sum Matrix addCommMonoid Multiset.map	—	AddMonoidHom.map_multiset_sum
transpose_pow 📖	mathematical	—	transpose Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring	—	MulOpposite.op_injective map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
transpose_sum 📖	mathematical	—	transpose Finset.sum Matrix addCommMonoid	—	map_sum AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
vecMul_sum 📖	mathematical	—	vecMul Finset.sum Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.addCommMonoid	—	Finset.sum_congr sum_apply Finset.mul_sum Finset.sum_apply Finset.sum_comm
zero_le_one_elem 📖	mathematical	—	Preorder.toLE Matrix one	—	one_apply_eq one_apply_ne
zero_le_one_row 📖	mathematical	—	Pi.hasLe Preorder.toLE Pi.instZero Matrix one	—	zero_le_one_elem

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStablyFiniteRing_iff 📖	mathematical	—	IsStablyFiniteRing MulOpposite instMulOne instAddCommMonoid	—	Matrix.map_one Matrix.ext Finset.op_sum Finset.sum_congr IsDedekindFiniteMonoid.of_injective MonoidHom.instMonoidHomClass Matrix.map_injective op_injective IsStablyFiniteRing.isDedekindFiniteMonoid instIsStablyFiniteRingMulOpposite

RingEquiv

Definitions

Name	Category	Theorems
mapMatrix 📖	CompOp	5 math math: map_det, mapMatrix_apply, mapMatrix_refl, mapMatrix_trans, mapMatrix_symm
mopMatrix 📖	CompOp	2 math math: mopMatrix_symm_apply, mopMatrix_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMatrix_apply 📖	mathematical	—	DFunLike.coe RingEquiv Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.add Distrib.toAdd EquivLike.toFunLike instEquivLike mapMatrix Matrix.map	—	—
mapMatrix_refl 📖	mathematical	—	mapMatrix refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd Matrix Matrix.instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.add	—	—
mapMatrix_symm 📖	mathematical	—	symm Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.add Distrib.toAdd mapMatrix	—	—
mapMatrix_trans 📖	mathematical	—	trans Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.add Distrib.toAdd mapMatrix	—	—
mopMatrix_apply 📖	mathematical	—	DFunLike.coe RingEquiv Matrix MulOpposite Matrix.instMulOfFintypeOfAddCommMonoid MulOpposite.instMul MulOpposite.instAddCommMonoid Matrix.add MulOpposite.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike instEquivLike mopMatrix MulOpposite.op Matrix.map Matrix.transpose MulOpposite.unop	—	—
mopMatrix_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite Matrix MulOpposite.instMul Matrix.instMulOfFintypeOfAddCommMonoid MulOpposite.instAddCommMonoid MulOpposite.instAdd Matrix.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup EquivLike.toFunLike instEquivLike symm mopMatrix Matrix.map Matrix.transpose MulOpposite.unop MulOpposite.op	—	—

RingHom

Definitions

Name	Category	Theorems
mapMatrix 📖	CompOp	16 math math: mapMatrix_id, mapMatrix_apply, Algebra.map_leftMulMatrix_localization, Algebra.traceMatrix_localizationLocalization, Matrix.SpecialLinearGroup.map_apply_coe, evalRingHom_mapMatrix_comp_polyToMatrix, Matrix.projVandermonde_map, evalRingHom_mapMatrix_comp_compRingEquiv, Polynomial.sylvester_map_map, map_adjugate, Matrix.mvPolynomialX_mapMatrix_eval, map_det, mapMatrix_comp, Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, matPolyEquiv_eq_X_pow_sub_C, Module.Basis.restrictScalars_toMatrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMatrix_apply 📖	mathematical	—	DFunLike.coe RingHom Matrix Matrix.nonAssocSemiring instFunLike mapMatrix Matrix.map	—	—
mapMatrix_comp 📖	mathematical	—	comp Matrix Matrix.nonAssocSemiring mapMatrix	—	—
mapMatrix_id 📖	mathematical	—	mapMatrix id Matrix Matrix.nonAssocSemiring	—	—

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_matrix 📖	mathematical	—	SetLike.coe Submodule Matrix Matrix.addCommMonoid Matrix.module setLike matrix Set.matrix	—	—

Subring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_matrix 📖	mathematical	—	SetLike.coe Subring Matrix Matrix.instRing instSetLike matrix AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero Matrix.addZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Ring.toSemiring AddSubmonoid.toAddSubsemigroup AddSubmonoid.matrix Subsemiring.toAddSubmonoid toSubsemiring	—	—

Subsemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_matrix 📖	mathematical	—	SetLike.coe Subsemiring Matrix Matrix.nonAssocSemiring instSetLike matrix AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero Matrix.addZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSubmonoid.toAddSubsemigroup AddSubmonoid.matrix toAddSubmonoid	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsStablyFiniteRingMulOpposite 📖	mathematical	—	IsStablyFiniteRing MulOpposite MulOpposite.instMulOne MulOpposite.instAddCommMonoid	—	IsDedekindFiniteMonoid.of_injective MonoidHom.instMonoidHomClass Matrix.transpose_one Matrix.map_one RingEquiv.map_mul RingEquiv.injective MulOpposite.instIsDedekindFiniteMonoid IsStablyFiniteRing.isDedekindFiniteMonoid

---

← Back to Index