ToLin

📁 Source: Mathlib/LinearAlgebra/Matrix/ToLin.lean

Statistics

Metric	Count
Definitions leftMulMatrix, toMatrix, toMatrix', toMatrixAlgEquiv, toMatrixAlgEquiv', toMatrixRight', mulVecBilin, mulVecLin, toLin, toLin', toLin'OfInv, toLinAlgEquiv, toLinAlgEquiv', toLinOfInv, toLinearEquivRight'OfInv, toLinearMapRight', vecMulBilin, vecMulLinear, end, linearMap, algEquivMatrix, algEquivMatrix', dotProductBilin, endVecAlgEquivMatrixEnd, endVecRingEquivMatrixEnd, matrixAlgEquivEndVecMulOpposite, matrixRingEquivEndVecMulOpposite, vecMulVecBilin	28
Theorems leftMulMatrix_apply, leftMulMatrix_eq_repr_mul, leftMulMatrix_injective, leftMulMatrix_mulVec_repr, smulTower_leftMulMatrix, smulTower_leftMulMatrix_algebraMap, smulTower_leftMulMatrix_algebraMap_eq, smulTower_leftMulMatrix_algebraMap_ne, smul_leftMulMatrix, toMatrix_lmul', toMatrix_lmul_eq, toMatrix_lsmul, isUnit_toMatrix'_iff, isUnit_toMatrix_iff, restrictScalars_toMatrix, toMatrix'_algebraMap, toMatrix'_apply, toMatrix'_comp, toMatrix'_id, toMatrix'_mul, toMatrix'_mulVec, toMatrix'_one, toMatrix'_symm, toMatrix'_toLin', toMatrixAlgEquiv'_apply, toMatrixAlgEquiv'_comp, toMatrixAlgEquiv'_id, toMatrixAlgEquiv'_mul, toMatrixAlgEquiv'_symm, toMatrixAlgEquiv'_toLinAlgEquiv', toMatrixAlgEquiv_apply, toMatrixAlgEquiv_apply', toMatrixAlgEquiv_comp, toMatrixAlgEquiv_id, toMatrixAlgEquiv_mul, toMatrixAlgEquiv_reindexRange, toMatrixAlgEquiv_symm, toMatrixAlgEquiv_toLinAlgEquiv, toMatrixAlgEquiv_transpose_apply, toMatrixAlgEquiv_transpose_apply', toMatrixRight'_comp, toMatrixRight'_id, toMatrix_algebraMap, toMatrix_apply, toMatrix_apply', toMatrix_basis_equiv, toMatrix_comp, toMatrix_eq_toMatrix', toMatrix_id, toMatrix_mul, toMatrix_mulVec_repr, toMatrix_one, toMatrix_pow, toMatrix_prodMap, toMatrix_reindexRange, toMatrix_singleton, toMatrix_smulBasis_left, toMatrix_smulBasis_right, toMatrix_smulRight, toMatrix_symm, toMatrix_toLin, toMatrix_toSpanSingleton, toMatrix_transpose_apply, toMatrix_transpose_apply', coe_mulVecLin, coe_vecMulLinear, isUnit_toLin'_iff, isUnit_toLin_iff, ker_mulVecLin_eq_bot_iff, ker_toLin'_eq_bot_iff, linearIndependent_cols_of_isUnit, linearIndependent_rows_of_isUnit, mulVecBilin_apply, mulVecLin_add, mulVecLin_apply, mulVecLin_mul, mulVecLin_one, mulVecLin_reindex, mulVecLin_submatrix, mulVecLin_transpose, mulVecLin_zero, mulVec_injective_iff, range_mulVecLin, range_toLin', repr_toLin, toLin'OfInv_apply, toLin'OfInv_symm_apply, toLin'_apply, toLin'_apply', toLin'_mul, toLin'_mul_apply, toLin'_one, toLin'_pow, toLin'_reindex, toLin'_submatrix, toLin'_symm, toLin'_toMatrix', toLinAlgEquiv'_apply, toLinAlgEquiv'_one, toLinAlgEquiv'_symm, toLinAlgEquiv'_toMatrixAlgEquiv', toLinAlgEquiv_apply, toLinAlgEquiv_mul, toLinAlgEquiv_one, toLinAlgEquiv_self, toLinAlgEquiv_symm, toLinAlgEquiv_toMatrixAlgEquiv, toLinOfInv_apply, toLinOfInv_symm_apply, toLin_apply, toLin_apply_eq_zero_iff, toLin_eq_toLin', toLin_finTwoProd, toLin_finTwoProd_apply, toLin_mul, toLin_mul_apply, toLin_one, toLin_pow, toLin_scalar, toLin_self, toLin_symm, toLin_toMatrix, toLinearEquivRight'OfInv_apply, toLinearEquivRight'OfInv_symm_apply, toLinearMapRight'_apply, toLinearMapRight'_mul, toLinearMapRight'_mul_apply, toLinearMapRight'_one, vecMulBilin_apply, vecMulLinear_apply, vecMulLinear_transpose, vecMul_injective_iff, end_apply, end_apply_apply, end_repr_apply, end_repr_symm_apply, linearMap_apply, linearMap_apply_apply, linearMap_repr_apply, linearMap_repr_symm_apply, injective_of_surjective_fin, dotProductBilin_apply_apply, endVecAlgEquivMatrixEnd_apply_apply, endVecAlgEquivMatrixEnd_symm_apply_apply, instIsStablyFiniteRingEndForallOfFinite, isStablyFiniteRing_iff_injective_of_surjective, isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd, range_vecMulLinear, toMatrix_distrib_mul_action_toLinearMap, vecMulVecBilin_apply_apply	150
Total	178

Algebra

Definitions

Name	Category	Theorems
leftMulMatrix 📖	CompOp	19 math math: LinearMap.restrictScalars_toMatrix, norm_eq_matrix_det, smul_leftMulMatrix, map_leftMulMatrix_localization, Module.Basis.toMatrix_smul, toMatrix_lmul_eq, leftMulMatrix_injective, PowerBasis.leftMulMatrix, charpoly_leftMulMatrix, smulTower_leftMulMatrix, leftMulMatrix_complex, smulTower_leftMulMatrix_algebraMap_ne, trace_eq_matrix_trace, smulTower_leftMulMatrix_algebraMap, leftMulMatrix_mulVec_repr, smulTower_leftMulMatrix_algebraMap_eq, Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, leftMulMatrix_eq_repr_mul, leftMulMatrix_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftMulMatrix_apply 📖	mathematical	—	DFunLike.coe AlgHom Matrix Matrix.semiring CommSemiring.toSemiring Matrix.instAlgebra id AlgHom.funLike leftMulMatrix LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring toModule LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype Module.End Module.End.instSemiring Module.End.instAlgebra toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero lmul	—	—
leftMulMatrix_eq_repr_mul 📖	mathematical	—	DFunLike.coe AlgHom Matrix Matrix.semiring CommSemiring.toSemiring Matrix.instAlgebra id AlgHom.funLike leftMulMatrix Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.instAddCommMonoid toModule Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype IsScalarTower.left leftMulMatrix_apply toMatrix_lmul'
leftMulMatrix_injective 📖	mathematical	—	Matrix DFunLike.coe AlgHom Matrix.semiring CommSemiring.toSemiring Matrix.instAlgebra id AlgHom.funLike leftMulMatrix	—	smulCommClass_self IsScalarTower.left mul_one LinearEquiv.injective RingHomInvPair.ids Finite.of_fintype
leftMulMatrix_mulVec_repr 📖	mathematical	—	Matrix.mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe AlgHom Matrix Matrix.semiring Matrix.instAlgebra id AlgHom.funLike leftMulMatrix Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.instAddCommMonoid toModule Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	LinearMap.toMatrix_mulVec_repr Finite.of_fintype to_smulCommClass
smulTower_leftMulMatrix 📖	mathematical	—	DFunLike.coe AlgHom Matrix Matrix.semiring CommSemiring.toSemiring instFintypeProd Matrix.instAlgebra id AlgHom.funLike leftMulMatrix Module.Basis.smulTower NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype to_smulCommClass IsScalarTower.right LinearMap.toMatrix_apply Module.Basis.smulTower_apply mul_smul_comm Module.Basis.smulTower_repr map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass mul_comm
smulTower_leftMulMatrix_algebraMap 📖	mathematical	—	DFunLike.coe AlgHom Matrix Matrix.semiring CommSemiring.toSemiring instFintypeProd Matrix.instAlgebra id AlgHom.funLike leftMulMatrix Module.Basis.smulTower NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule RingHom RingHom.instFunLike algebraMap Matrix.blockDiagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.ext smulTower_leftMulMatrix AlgHom.commutes Matrix.blockDiagonal_apply Matrix.algebraMap_matrix_apply map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
smulTower_leftMulMatrix_algebraMap_eq 📖	mathematical	—	DFunLike.coe AlgHom Matrix Matrix.semiring CommSemiring.toSemiring instFintypeProd Matrix.instAlgebra id AlgHom.funLike leftMulMatrix Module.Basis.smulTower NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule RingHom RingHom.instFunLike algebraMap	—	smulTower_leftMulMatrix_algebraMap Matrix.blockDiagonal_apply_eq
smulTower_leftMulMatrix_algebraMap_ne 📖	mathematical	—	DFunLike.coe AlgHom Matrix Matrix.semiring CommSemiring.toSemiring instFintypeProd Matrix.instAlgebra id AlgHom.funLike leftMulMatrix Module.Basis.smulTower NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule RingHom RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	smulTower_leftMulMatrix_algebraMap Matrix.blockDiagonal_apply_ne
smul_leftMulMatrix 📖	mathematical	—	DFunLike.coe AlgHom Matrix Matrix.semiring CommSemiring.toSemiring Matrix.instAlgebra id AlgHom.funLike leftMulMatrix Module.Basis NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring toModule Module.Basis.instSMul	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype IsScalarTower.left LinearMap.toMatrix_apply to_smulCommClass IsScalarTower.right RingHomCompTriple.ids mul_smul_comm inv_smul_smul
toMatrix_lmul' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring toModule Matrix LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype AlgHom Module.End Module.End.instSemiring Module.End.instAlgebra toSMul id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike lmul Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype IsScalarTower.left LinearMap.toMatrix_apply' to_smulCommClass IsScalarTower.right
toMatrix_lmul_eq 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring toModule Matrix LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype LinearMap.mulLeft to_smulCommClass AlgHom Matrix.semiring Matrix.instAlgebra id AlgHom.funLike leftMulMatrix	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype to_smulCommClass
toMatrix_lsmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring toModule Matrix LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype AlgHom Module.End Module.End.instSemiring id Module.End.instAlgebra IsScalarTower.to_smulCommClass' IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero toSMul AlgHom.funLike lsmul Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	toMatrix_distrib_mul_action_toLinearMap

LinearMap

Definitions

Name	Category	Theorems
toMatrix 📖	CompOp	88 math math: restrictScalars_toMatrix, charpoly_def, detAux_def'', Module.Basis.end_repr_apply, Polynomial.toMatrix_sylvesterMap', toMatrix_apply', BilinForm.toMatrix_compRight, toMatrix_one, toMatrix_distrib_mul_action_toLinearMap, toMatrix_rotation, toMatrix_baseChange, trace_eq_matrix_trace_of_finset, Algebra.toMatrix_lmul_eq, toMatrix_symm, TensorProduct.toMatrix_assoc, toMatrix_id, toMatrix_transpose, IsBaseChange.endHom_toMatrix, Matrix.toLin_symm, toMatrix₂_compl₂, toMatrix₂_comp, isNilpotent_toMatrix_iff, det_eq_det_toMatrix_of_finset, toMatrix_reindexRange, toMatrix_smulBasis_left, BilinForm.toMatrix_comp, toMatrixOrthonormal_symm_apply, toMatrix_mulVec_repr, toMatrix_innerₛₗ_apply, linearMap_toMatrix_mul_basis_toMatrix, polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, toMatrix_transpose_apply, toMatrix_dualTensorHom, toMatrix_smulBasis_right, Module.Basis.linearMap_repr_apply, mul_basis_toMatrix, toMatrix_algebraMap, spectrum_toMatrix, toMatrix_mul, toMatrix₂_compl₁₂, BilinForm.toMatrix_compRight, detAux_def', toMatrix_transpose_apply', IsBaseChange.linearMapLeftRightHom_toMatrix, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, toMatrix_smulRight, minpoly_toMatrix, toMatrixOrthonormal_apply, Algebra.toMatrix_lmul', toMatrix_prodMap, LinearEquiv.isUnit_det, toMatrix_directSum_collectedBasis_eq_blockDiagonal', InnerProductSpace.toMatrix_rankOne, isUnit_toMatrix_iff, BilinForm.toMatrix_compLeft, trace_eq_matrix_trace, Algebra.toMatrix_lsmul, toMatrix_innerSL_apply, toMatrix_comp, Module.Basis.toMatrix_eq_toMatrix_constr, Matrix.toLin_toMatrix, Polynomial.toMatrix_sylvesterMap, Complex.toMatrix_conjAe, toMatrix_toSpanSingleton, toMatrix_singleton, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, toMatrix_basis_equiv, BilinForm.toMatrix_compLeft, toMatrix_eq_toMatrix', toMatrix_pow, BilinForm.toMatrix_comp, basis_toMatrix_mul_linearMap_toMatrix, Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix, toMatrix_adjoint, diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, det_toMatrix, basis_toMatrix_mul, posSemidef_toMatrix_iff, TensorProduct.toMatrix_comm, traceAux_def, Algebra.leftMulMatrix_apply, toMatrix_apply, TensorProduct.toMatrix_map, toMatrix_id_eq_basis_toMatrix, det_toMatrix_eq_det_toMatrix, charpoly_toMatrix, toMatrix_toLin, polyCharpolyAux_map_eq_toMatrix_charpoly
toMatrix' 📖	CompOp	30 math math: Matrix.toLin'_symm, QuadraticMap.toMatrix'_comp, spectrum_toMatrix', toMatrix₂'_compl₁₂, toMatrix'_toLin', Matrix.linfty_opNNNorm_toMatrix, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, lieEquivMatrix'_apply, minpoly_toMatrix', toMatrix'_algebraMap, BilinForm.toMatrix'_compLeft, toMatrix'_apply, toMatrix'_symm, QuadraticMap.discr_comp, toMatrix'_mul, toMatrix'_intrinsicStar, toMatrix'_comp, isUnit_toMatrix'_iff, toMatrix'_id, BilinForm.toMatrix'_comp, Matrix.linfty_opNorm_toMatrix, IntrinsicStar.isSelfAdjoint_iff_toMatrix', toMatrix₂'_compl₂, det_toMatrix', toMatrix₂'_comp, toMatrix_eq_toMatrix', toMatrix'_one, Matrix.toLin'_toMatrix', toMatrix'_mulVec, BilinForm.toMatrix'_compRight
toMatrixAlgEquiv 📖	CompOp	13 math math: toMatrixAlgEquiv_comp, toMatrixAlgEquiv_toLinAlgEquiv, toMatrixAlgEquiv_apply, detAux_def, toMatrixAlgEquiv_id, toMatrixAlgEquiv_symm, toMatrixAlgEquiv_apply', toMatrixAlgEquiv_reindexRange, toMatrixAlgEquiv_mul, toMatrixAlgEquiv_transpose_apply, Matrix.toLinAlgEquiv_toMatrixAlgEquiv, Matrix.toLinAlgEquiv_symm, toMatrixAlgEquiv_transpose_apply'
toMatrixAlgEquiv' 📖	CompOp	8 math math: toMatrixAlgEquiv'_mul, toMatrixAlgEquiv'_id, toMatrixAlgEquiv'_apply, toMatrixAlgEquiv'_toLinAlgEquiv', toMatrixAlgEquiv'_symm, Matrix.toLinAlgEquiv'_toMatrixAlgEquiv', Matrix.toLinAlgEquiv'_symm, toMatrixAlgEquiv'_comp
toMatrixRight' 📖	CompOp	2 math math: toMatrixRight'_id, toMatrixRight'_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_toMatrix'_iff 📖	mathematical	—	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' Module.End.instMonoid	—	isUnit_map_iff Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass isLocalHom_equiv RingEquivClass.toMulEquivClass AlgEquivClass.toRingEquivClass
isUnit_toMatrix_iff 📖	mathematical	—	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype Module.End.instMonoid	—	isUnit_map_iff smulCommClass_self IsScalarTower.left MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass isLocalHom_equiv RingEquivClass.toMulEquivClass AlgEquivClass.toRingEquivClass
restrictScalars_toMatrix 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix instFintypeProd Finite.instProd Finite.of_fintype Module.Basis.smulTower' Algebra.toModule restrictScalars IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toSMul Equiv Equiv.instEquivLike Matrix.comp Matrix.map AlgHom Matrix.semiring Matrix.instAlgebra Algebra.id AlgHom.funLike Algebra.leftMulMatrix	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.instProd Finite.of_fintype IsScalarTower.compatibleSMul Module.Basis.equivFun_symm_apply Finset.sum_congr Module.Basis.smulTower'_apply Fintype.sum_single_smul one_smul map_smul SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass Module.Basis.smulTower'_repr SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Algebra.to_smulCommClass IsScalarTower.right mul_comm
toMatrix'_algebraMap 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' RingHom Module.End Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra Algebra.toSMul Pi.isScalarTower IsScalarTower.right Matrix.nonAssocSemiring Matrix.scalar	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass toMatrix'_id Matrix.smul_eq_diagonal_mul mul_one
toMatrix'_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' instFunLike Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass
toMatrix'_comp 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' comp RingHomCompTriple.ids Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	RingHomCompTriple.ids RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Matrix.toLin'_mul Matrix.toLin'_toMatrix' toMatrix'_toLin'
toMatrix'_id 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' id Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Matrix.ext RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Matrix.one_apply toMatrix'_apply id_apply Pi.single_apply
toMatrix'_mul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' Module.End.instMul Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	toMatrix'_comp
toMatrix'_mulVec 📖	mathematical	—	Matrix.mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' instFunLike	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Matrix.toLin'_apply Matrix.toLin'_toMatrix'
toMatrix'_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' Module.End.instOne Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toMatrix'_id
toMatrix'_symm 📖	mathematical	—	LinearEquiv.symm LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module RingHomInvPair.ids toMatrix' Matrix.toLin'	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass
toMatrix'_toLin' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' Matrix.toLin'	—	LinearEquiv.apply_symm_apply Function.smulCommClass Algebra.to_smulCommClass RingHomInvPair.ids
toMatrixAlgEquiv'_apply 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Algebra.toSMul Pi.isScalarTower IsScalarTower.right Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv' instFunLike Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right
toMatrixAlgEquiv'_comp 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Algebra.toSMul Pi.isScalarTower IsScalarTower.right Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv' comp RingHomCompTriple.ids Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	toMatrix'_comp
toMatrixAlgEquiv'_id 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Algebra.toSMul Pi.isScalarTower IsScalarTower.right Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv' id Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toMatrix'_id
toMatrixAlgEquiv'_mul 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Algebra.toSMul Pi.isScalarTower IsScalarTower.right Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv' Module.End.instMul Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	toMatrixAlgEquiv'_comp
toMatrixAlgEquiv'_symm 📖	mathematical	—	AlgEquiv.symm LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Algebra.toSMul Pi.isScalarTower IsScalarTower.right Matrix.instAlgebra toMatrixAlgEquiv' Matrix.toLinAlgEquiv'	—	Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right
toMatrixAlgEquiv'_toLinAlgEquiv' 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Algebra.toSMul Pi.isScalarTower IsScalarTower.right Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv' Matrix.toLinAlgEquiv'	—	AlgEquiv.apply_symm_apply Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right
toMatrixAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr instFunLike Module.Basis Module.Basis.instFunLike	—	smulCommClass_self IsScalarTower.left RingHomInvPair.ids toMatrix_apply Finite.of_fintype
toMatrixAlgEquiv_apply' 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr instFunLike Module.Basis Module.Basis.instFunLike	—	toMatrixAlgEquiv_apply
toMatrixAlgEquiv_comp 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv comp RingHomCompTriple.ids Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid	—	smulCommClass_self IsScalarTower.left RingHomCompTriple.ids Finite.of_fintype RingHomInvPair.ids toMatrix_comp
toMatrixAlgEquiv_id 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv id Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	smulCommClass_self IsScalarTower.left Finite.of_fintype toMatrix_one toMatrix_mul toMatrix_id
toMatrixAlgEquiv_mul 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv Module.End.instMul Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid	—	smulCommClass_self IsScalarTower.left RingHomCompTriple.ids Module.End.mul_eq_comp toMatrixAlgEquiv_comp
toMatrixAlgEquiv_reindexRange 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix Set.Elem Set.range Module.Basis Module.Basis.instFunLike Module.End.instSemiring Matrix.semiring Set.fintypeRange PLift.fintype Set Set.instMembership Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv Module.Basis.reindexRange Set.mem_range_self	—	smulCommClass_self IsScalarTower.left Set.mem_range_self RingHomInvPair.ids toMatrixAlgEquiv_apply Module.Basis.reindexRange_self Module.Basis.reindexRange_repr
toMatrixAlgEquiv_symm 📖	mathematical	—	AlgEquiv.symm LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.instAlgebra toMatrixAlgEquiv Matrix.toLinAlgEquiv	—	smulCommClass_self IsScalarTower.left
toMatrixAlgEquiv_toLinAlgEquiv 📖	mathematical	—	DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv Matrix.toLinAlgEquiv	—	smulCommClass_self IsScalarTower.left Matrix.toLinAlgEquiv_symm AlgEquiv.symm_apply_apply
toMatrixAlgEquiv_transpose_apply 📖	mathematical	—	Matrix.transpose DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr instFunLike Module.Basis Module.Basis.instFunLike	—	smulCommClass_self IsScalarTower.left RingHomInvPair.ids toMatrix_apply Finite.of_fintype
toMatrixAlgEquiv_transpose_apply' 📖	mathematical	—	Matrix.transpose DFunLike.coe AlgEquiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.instAlgebra AlgEquiv.instFunLike toMatrixAlgEquiv Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr instFunLike Module.Basis Module.Basis.instFunLike	—	toMatrixAlgEquiv_transpose_apply
toMatrixRight'_comp 📖	mathematical	—	DFunLike.coe LinearEquiv MulOpposite MulOpposite.instSemiring RingHom.id MulOpposite.instNonAssocSemiring Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Semiring.toOppositeModule Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsScalarTower.left Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrixRight' comp RingHomCompTriple.ids Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	LinearEquiv.injective Function.smulCommClass SMulCommClass.opposite_mid IsScalarTower.left RingHomInvPair.ids RingHomCompTriple.ids LinearEquiv.symm_apply_apply Matrix.toLinearMapRight'_mul comp.congr_simp
toMatrixRight'_id 📖	mathematical	—	DFunLike.coe LinearEquiv MulOpposite MulOpposite.instSemiring RingHom.id MulOpposite.instNonAssocSemiring Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Semiring.toOppositeModule Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsScalarTower.left Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrixRight' id Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	LinearEquiv.injective Function.smulCommClass SMulCommClass.opposite_mid IsScalarTower.left RingHomInvPair.ids LinearEquiv.symm_apply_apply Matrix.toLinearMapRight'_one
toMatrix_algebraMap 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype RingHom Module.End Module.End.instSemiring RingHom.instFunLike algebraMap Module.End.instAlgebra Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.nonAssocSemiring Matrix.scalar	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype IsScalarTower.left map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass toMatrix_id Matrix.smul_eq_diagonal_mul mul_one
toMatrix_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr instFunLike Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype Module.Basis.equivFun_symm_apply Fintype.sum_single_smul one_smul
toMatrix_apply' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr instFunLike Module.Basis Module.Basis.instFunLike	—	toMatrix_apply
toMatrix_basis_equiv 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype LinearEquiv.toLinearMap Module.Basis.equiv Equiv.refl Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype toMatrix_apply Module.Basis.equiv_apply Module.Basis.repr_self Finsupp.single_apply
toMatrix_comp 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix comp RingHomCompTriple.ids Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self RingHomCompTriple.ids Finite.of_fintype LinearEquiv.arrowCongr_comp Function.smulCommClass Algebra.to_smulCommClass toMatrix'_comp
toMatrix_eq_toMatrix' 📖	mathematical	—	toMatrix Finite.of_fintype Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule Pi.basisFun toMatrix'	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype
toMatrix_id 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype id Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype toMatrix_apply Module.Basis.repr_self Finsupp.single_apply
toMatrix_mul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype Module.End.instMul Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype RingHomCompTriple.ids Module.End.mul_eq_comp toMatrix_comp
toMatrix_mulVec_repr 📖	mathematical	—	Matrix.mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr instFunLike	—	RingHomInvPair.ids smulCommClass_self Function.smulCommClass Algebra.to_smulCommClass Matrix.toLin'_apply Finite.of_fintype toMatrix.eq_1 LinearEquiv.trans_apply Matrix.toLin'_toMatrix' LinearEquiv.arrowCongr_apply Module.Basis.equivFun_apply LinearEquiv.symm_apply_apply
toMatrix_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype Module.End.instOne Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toMatrix_id
toMatrix_pow 📖	mathematical	—	Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype Module.End.instMonoid	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype pow_zero toMatrix_one pow_succ toMatrix_mul
toMatrix_prodMap 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Prod.instAddCommMonoid Prod.instModule Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix instFintypeSum Finite.instSum Finite.of_fintype Module.Basis.prod prodMap Matrix.fromBlocks Matrix.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.instSum Finite.of_fintype Module.Basis.equivFun_symm_apply Finset.sum_congr Module.Basis.prod_apply Fintype.sum_single_smul one_smul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
toMatrix_reindexRange 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix Set.Elem Set.range Module.Basis Module.Basis.instFunLike addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Set.fintypeRange PLift.fintype Finite.Set.finite_range Set Set.instMembership Module.Basis.reindexRange Set.mem_range_self	—	RingHomInvPair.ids smulCommClass_self Finite.Set.finite_range Set.mem_range_self toMatrix_apply Module.Basis.reindexRange_self Module.Basis.reindexRange_repr
toMatrix_singleton 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Unique.fintype Finite.of_fintype decidableEq_of_subsingleton Unique.instSubsingleton Module.Basis.singleton instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype Unique.instSubsingleton Module.Basis.equivFun_symm_apply Finset.sum_congr Finset.univ_unique Module.Basis.singleton_apply mul_one Finset.sum_pi_single' Module.Basis.singleton_repr
toMatrix_smulBasis_left 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Module.Basis Module.Basis.instSMul comp RingHomCompTriple.ids DistribSMul.toLinearMap DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid	—	RingHomInvPair.ids smulCommClass_self
toMatrix_smulBasis_right 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Module.Basis Module.Basis.instSMul comp RingHomCompTriple.ids DistribSMul.toLinearMap DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	RingHomInvPair.ids smulCommClass_self
toMatrix_smulRight 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix smulRight IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.vecMulVec Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr instFunLike Module.Basis Module.Basis.instFunLike	—	Matrix.ext RingHomInvPair.ids smulCommClass_self IsScalarTower.left toMatrix_apply map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass mul_comm
toMatrix_symm 📖	mathematical	—	LinearEquiv.symm LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule RingHomInvPair.ids toMatrix Matrix.toLin	—	RingHomInvPair.ids smulCommClass_self
toMatrix_toLin 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Matrix.toLin	—	RingHomInvPair.ids smulCommClass_self Matrix.toLin_symm LinearEquiv.symm_apply_apply
toMatrix_toSpanSingleton 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix toSpanSingleton Matrix.vecMulVec Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr Module.Basis Module.Basis.instFunLike	—	Matrix.ext RingHomInvPair.ids smulCommClass_self toMatrix_apply map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass mul_comm
toMatrix_transpose_apply 📖	mathematical	—	Matrix.transpose DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr instFunLike Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids smulCommClass_self toMatrix_apply
toMatrix_transpose_apply' 📖	mathematical	—	Matrix.transpose DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr instFunLike Module.Basis Module.Basis.instFunLike	—	toMatrix_transpose_apply

Matrix

Definitions

Name	Category	Theorems
mulVecBilin 📖	CompOp	1 math math: mulVecBilin_apply
mulVecLin 📖	CompOp	20 math math: coe_mulVecLin, mulVecLin_apply, GeneralLinearGroup.coe_toLin, ker_mulVecLin_conjTranspose_mul_self, mulVecLin_add, linfty_opNNNorm_eq_opNNNorm, ker_mulVecLin_eq_bot_iff, mulVecLin_zero, mulVecLin_one, ker_mulVecLin_transpose_mul_self, range_mulVecLin, toLin'_apply', mulVecLin_transpose, charpoly_mulVecLin, mulVecLin_submatrix, vecMulLinear_transpose, linfty_opNorm_eq_opNorm, mulVecLin_reindex, GeneralLinearGroup.toLin_apply, mulVecLin_mul
toLin 📖	CompOp	61 math math: toLin_kronecker, LinearMap.toMatrix₂_mul, repr_toLin, toLin_mul_apply, isAdjointPair_toLinearMap₂, LinearMap.toMatrix_symm, Module.Basis.toLin_toMatrix, toLin_symm, BilinForm.mul_toMatrix_mul, Module.Basis.linearMap_apply, toLinearMap₂_compl₁₂, toLin_scalar, rank_eq_finrank_range_toLin, toLin_mul, toLin_pow, toLin_self, charpoly_toLin, toLin_apply_eq_zero_iff, Module.Basis.end_apply, ker_toLin_eq_bot, range_toLin_eq_top, toLin_finTwoProd_apply, LinearMap.mul_toMatrix₂, mul_basis_toMatrix, isUnit_toLin_iff, toLinOfInv_symm_apply, toLin_apply, toLin_conjTranspose, Orientation.rotation_eq_matrix_toLin, spectrum_toLin, toEuclideanLin_eq_toLin, Module.Basis.end_repr_symm_apply, LinearMap.mul_toMatrix₂_mul, LinearMap.BilinForm.mul_toMatrix_mul, LinearMap.BilinForm.toMatrix_mul, LinearMap.BilinForm.mul_toMatrix, BilinForm.toMatrix_mul, trace_toLin_eq, toLinOfInv_apply, toLin_finTwoProd_toContinuousLinearMap, toLin_toMatrix, toLin_finTwoProd, SpecialLinearGroup.toLin_equiv.toLinearMap_eq, Module.Basis.linearMap_repr_symm_apply, toLin_one, toLin_transpose, BilinForm.mul_toMatrix, toLin_eq_toLin', LinearEquiv.ofIsUnitDet_symm_apply, maxGenEigenspace_toLin_diagonal_eq_eigenspace, toEuclideanLin_eq_toLin_orthonormal, iSup_eigenspace_toLin_diagonal_eq_top, minpoly_toLin, basis_toMatrix_mul, LinearMap.det_toLin, hasEigenvector_toLin_diagonal, toLpLin_eq_toLin, toBilin_comp, LinearMap.toMatrix_toLin, toLinearEquiv_apply, hasEigenvalue_toLin_diagonal_iff
toLin' 📖	CompOp	64 math math: toLin'_symm, iSup_eigenspace_toLin'_diagonal_eq_top, toLinearMap₂'_comp, intrinsicStar_toLin', SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, Real.smul_map_diagonal_volume_pi, LinearMap.rank_diagonal, toLin'_mul_apply, LinearMap.toMatrix'_toLin', SpecialLinearGroup.toLin'_symm_to_linearMap, Real.map_matrix_volume_pi_eq_smul_volume_pi, isNilpotent_toLin'_iff, toLinearEquiv'_symm_apply, LinearMap.BilinForm.mul_toMatrix'_mul, piLp_ofLp_toEuclideanLin, SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux, isUnit_toLin'_iff, toLin'_mul, ofLp_toLpLin, LinearMap.det_toLin', hasEigenvector_toLin'_diagonal, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, toLin'_reindex, toLpLin_toLp, IntrinsicStar.isSelfAdjoint_toLin'_iff, LinearMap.toMatrix'_symm, range_toLin', LinearMap.mul_toMatrix', diagonal_toLin', charpoly_toLin', toLin'_pow, minpoly_toLin', isAdjointPair_toLinearMap₂', toLin'_apply', ker_toLin'_eq_bot_iff, LinearMap.BilinForm.mul_toMatrix', ker_diagonal_toLin', toLin'_one, trace_toLin'_eq, toLin'OfInv_symm_apply, toLinearEquiv'_apply, toBilin'_comp, lieEquivMatrix'_symm_apply, proj_diagonal, SpecialLinearGroup.toLin'_to_linearMap, LinearMap.mul_toMatrix₂'_mul, LinearMap.toMatrix₂'_mul, hasEigenvalue_toLin'_diagonal_iff, toLin'_submatrix, toLin_eq_toLin', LinearMap.BilinForm.toMatrix'_mul, toLin'OfInv_apply, range_diagonal, SpecialLinearGroup.toLin'_symm_apply, maxGenEigenspace_toLin'_diagonal_eq_eigenspace, toLin'_apply, toEuclideanLin_toLp, toLin'_toMatrix', Real.volume_preserving_transvectionStruct, diagonal_comp_single, rank_vecMulVec, SimpleGraph.mem_ker_toLin'_lapMatrix_of_connectedComponent, SpecialLinearGroup.toLin'_apply, spectrum_toLin'
toLin'OfInv 📖	CompOp	2 math math: toLin'OfInv_symm_apply, toLin'OfInv_apply
toLinAlgEquiv 📖	CompOp	8 math math: toLinAlgEquiv_one, LinearMap.toMatrixAlgEquiv_toLinAlgEquiv, toLinAlgEquiv_mul, LinearMap.toMatrixAlgEquiv_symm, toLinAlgEquiv_apply, toLinAlgEquiv_self, toLinAlgEquiv_toMatrixAlgEquiv, toLinAlgEquiv_symm
toLinAlgEquiv' 📖	CompOp	6 math math: toLinAlgEquiv'_apply, LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv', LinearMap.toMatrixAlgEquiv'_symm, toLinAlgEquiv'_toMatrixAlgEquiv', toLinAlgEquiv'_one, toLinAlgEquiv'_symm
toLinOfInv 📖	CompOp	2 math math: toLinOfInv_symm_apply, toLinOfInv_apply
toLinearEquivRight'OfInv 📖	CompOp	2 math math: toLinearEquivRight'OfInv_symm_apply, toLinearEquivRight'OfInv_apply
toLinearMapRight' 📖	CompOp	6 math math: toLinearMapRight'_mul, toLinearEquivRight'OfInv_symm_apply, toLinearMapRight'_mul_apply, toLinearMapRight'_apply, toLinearEquivRight'OfInv_apply, toLinearMapRight'_one
vecMulBilin 📖	CompOp	1 math math: vecMulBilin_apply
vecMulLinear 📖	CompOp	5 math math: range_vecMulLinear, coe_vecMulLinear, vecMulLinear_apply, mulVecLin_transpose, vecMulLinear_transpose

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mulVecLin 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike mulVecLin mulVec	—	—
coe_vecMulLinear 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike vecMulLinear vecMul	—	—
isUnit_toLin'_iff 📖	mathematical	—	IsUnit LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Module.End.instMonoid DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' semiring	—	isUnit_map_iff Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass isLocalHom_equiv RingEquivClass.toMulEquivClass AlgEquivClass.toRingEquivClass
isUnit_toLin_iff 📖	mathematical	—	IsUnit LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	isUnit_map_iff smulCommClass_self IsScalarTower.left MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass isLocalHom_equiv RingEquivClass.toMulEquivClass AlgEquivClass.toRingEquivClass
ker_mulVecLin_eq_bot_iff 📖	mathematical	—	LinearMap.ker CommSemiring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id mulVecLin Bot.bot Submodule Submodule.instBot Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
ker_toLin'_eq_bot_iff 📖	mathematical	—	LinearMap.ker CommSemiring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' Bot.bot Submodule Submodule.instBot Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	ker_mulVecLin_eq_bot_iff
linearIndependent_cols_of_isUnit 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring	LinearIndependent col Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule	—	mulVec_injective_iff mulVec_injective_of_isUnit
linearIndependent_rows_of_isUnit 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	LinearIndependent row Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule	—	vecMul_injective_iff vecMul_injective_of_isUnit
mulVecBilin_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module LinearMap.instFunLike Matrix addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction mulVecBilin mulVec	—	Function.smulCommClass
mulVecLin_add 📖	mathematical	—	mulVecLin Matrix add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring LinearMap RingHom.id Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instAdd	—	LinearMap.ext add_mulVec
mulVecLin_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike mulVecLin mulVec	—	—
mulVecLin_mul 📖	mathematical	—	mulVecLin Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid LinearMap.comp Pi.addCommMonoid Pi.Function.module Semiring.toModule RingHom.id RingHomCompTriple.ids	—	LinearMap.ext RingHomCompTriple.ids mulVec_mulVec
mulVecLin_one 📖	mathematical	—	mulVecLin Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne LinearMap.id Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module Semiring.toModule	—	LinearMap.pi_ext' Finite.of_fintype LinearMap.ext_ring RingHomCompTriple.ids mulVec_single smul_ite one_smul smul_zero Pi.single_apply
mulVecLin_reindex 📖	mathematical	—	mulVecLin DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike reindex LinearMap.comp CommSemiring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.funCongrLeft Equiv.symm	—	mulVecLin_submatrix
mulVecLin_submatrix 📖	mathematical	—	mulVecLin submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike LinearMap.comp CommSemiring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id RingHomCompTriple.ids LinearMap.funLeft Equiv.symm	—	LinearMap.ext RingHomCompTriple.ids submatrix_mulVec_equiv
mulVecLin_transpose 📖	mathematical	—	mulVecLin transpose vecMulLinear CommSemiring.toSemiring	—	LinearMap.ext mulVec_transpose
mulVecLin_zero 📖	mathematical	—	mulVecLin Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring LinearMap RingHom.id Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instZero	—	LinearMap.ext zero_mulVec
mulVec_injective_iff 📖	mathematical	—	mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring LinearIndependent col Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module Semiring.toModule	—	vecMul_transpose
range_mulVecLin 📖	mathematical	—	LinearMap.range CommSemiring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id RingHomSurjective.ids mulVecLin Submodule.span Set.range col	—	RingHomSurjective.ids vecMulLinear_transpose range_vecMulLinear row_transpose
range_toLin' 📖	mathematical	—	LinearMap.range CommSemiring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id RingHomSurjective.ids DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' Submodule.span Set.range col	—	range_mulVecLin
repr_toLin 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr LinearMap LinearMap.instFunLike Matrix addCommMonoid LinearMap.addCommMonoid module LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction toLin mulVec	—	RingHomInvPair.ids smulCommClass_self LinearMap.toMatrix_mulVec_repr LinearMap.toMatrix_toLin
toLin'OfInv_apply 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Pi.addCommMonoid Pi.Function.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike toLin'OfInv LinearMap LinearMap.instFunLike addCommMonoid LinearMap.addCommMonoid module LinearMap.module DFinsupp.instEquivLikeLinearEquiv toLin'	—	RingHomInvPair.ids
toLin'OfInv_symm_apply 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Pi.addCommMonoid Pi.Function.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toLin'OfInv LinearMap LinearMap.instFunLike addCommMonoid LinearMap.addCommMonoid module LinearMap.module DFinsupp.instEquivLikeLinearEquiv toLin'	—	RingHomInvPair.ids
toLin'_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Matrix addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' mulVec	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass
toLin'_apply' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' mulVecLin	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass
toLin'_mul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap.comp RingHomCompTriple.ids	—	mulVecLin_mul
toLin'_mul_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Matrix addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass RingHomCompTriple.ids toLin'_mul LinearMap.comp_apply
toLin'_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne LinearMap.id	—	mulVecLin_one
toLin'_pow 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' Monoid.toNatPow semiring Module.End.instMonoid	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass pow_zero toLin'_one pow_succ RingHomCompTriple.ids toLin'_mul Module.End.mul_eq_comp
toLin'_reindex 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' Equiv Equiv.instEquivLike reindex LinearMap.comp RingHomCompTriple.ids LinearEquiv.toLinearMap LinearEquiv.funCongrLeft Equiv.symm	—	mulVecLin_reindex
toLin'_submatrix 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' submatrix Equiv Equiv.instEquivLike LinearMap.comp RingHomCompTriple.ids LinearMap.funLeft Equiv.symm	—	mulVecLin_submatrix
toLin'_symm 📖	mathematical	—	LinearEquiv.symm Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id RingHomInvPair.ids toLin' LinearMap.toMatrix'	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass
toLin'_toMatrix' 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' LinearMap.toMatrix'	—	LinearEquiv.apply_symm_apply Function.smulCommClass Algebra.to_smulCommClass RingHomInvPair.ids
toLinAlgEquiv'_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike AlgEquiv Matrix semiring Module.End.instSemiring instAlgebra Algebra.id Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.toSMul Pi.isScalarTower IsScalarTower.right AlgEquiv.instFunLike toLinAlgEquiv' mulVec	—	Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right
toLinAlgEquiv'_one 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule semiring Module.End.instSemiring instAlgebra Algebra.id Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.toSMul Pi.isScalarTower IsScalarTower.right AlgEquiv.instFunLike toLinAlgEquiv' one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne LinearMap.id	—	toLin'_one
toLinAlgEquiv'_symm 📖	mathematical	—	AlgEquiv.symm Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule semiring Module.End.instSemiring instAlgebra Algebra.id Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.toSMul Pi.isScalarTower IsScalarTower.right toLinAlgEquiv' LinearMap.toMatrixAlgEquiv'	—	Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right
toLinAlgEquiv'_toMatrixAlgEquiv' 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule semiring Module.End.instSemiring instAlgebra Algebra.id Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.toSMul Pi.isScalarTower IsScalarTower.right AlgEquiv.instFunLike toLinAlgEquiv' LinearMap.toMatrixAlgEquiv'	—	AlgEquiv.apply_symm_apply Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right
toLinAlgEquiv_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike AlgEquiv Matrix semiring Module.End.instSemiring instAlgebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgEquiv.instFunLike toLinAlgEquiv Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids Finite.of_fintype Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right toLinAlgEquiv'_apply Module.Basis.equivFun_symm_apply
toLinAlgEquiv_mul 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring semiring Module.End.instSemiring instAlgebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgEquiv.instFunLike toLinAlgEquiv instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid LinearMap.comp RingHomCompTriple.ids	—	smulCommClass_self IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids Finite.of_fintype toLin_mul
toLinAlgEquiv_one 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring semiring Module.End.instSemiring instAlgebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgEquiv.instFunLike toLinAlgEquiv one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne LinearMap.id	—	smulCommClass_self IsScalarTower.left LinearMap.toMatrixAlgEquiv_id toLinAlgEquiv_toMatrixAlgEquiv
toLinAlgEquiv_self 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike AlgEquiv Matrix semiring Module.End.instSemiring instAlgebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgEquiv.instFunLike toLinAlgEquiv Module.Basis Module.Basis.instFunLike Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	toLin_self
toLinAlgEquiv_symm 📖	mathematical	—	AlgEquiv.symm Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring semiring Module.End.instSemiring instAlgebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero toLinAlgEquiv LinearMap.toMatrixAlgEquiv	—	smulCommClass_self IsScalarTower.left
toLinAlgEquiv_toMatrixAlgEquiv 📖	mathematical	—	DFunLike.coe AlgEquiv Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring semiring Module.End.instSemiring instAlgebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgEquiv.instFunLike toLinAlgEquiv LinearMap.toMatrixAlgEquiv	—	smulCommClass_self IsScalarTower.left toLinAlgEquiv_symm AlgEquiv.apply_symm_apply
toLinOfInv_apply 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike toLinOfInv LinearMap LinearMap.instFunLike addCommMonoid LinearMap.addCommMonoid module Semiring.toModule LinearMap.module DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype	—	RingHomInvPair.ids
toLinOfInv_symm_apply 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toLinOfInv LinearMap LinearMap.instFunLike addCommMonoid LinearMap.addCommMonoid module Semiring.toModule LinearMap.module DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype	—	RingHomInvPair.ids
toLin_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero mulVec Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids Finite.of_fintype Function.smulCommClass Algebra.to_smulCommClass toLin'_apply Module.Basis.equivFun_symm_apply
toLin_apply_eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike Finsupp.instAddCommMonoid Finsupp.module Module.Basis.repr	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype toLin_apply Fintype.linearIndependent_iff Module.Basis.linearIndependent Finset.sum_congr zero_smul Finset.sum_const_zero
toLin_eq_toLin' 📖	mathematical	—	toLin Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule Pi.basisFun Finite.of_fintype toLin'	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype
toLin_finTwoProd 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Prod.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instModule Semiring.toModule addCommMonoid LinearMap.addCommMonoid module LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Fin.fintype Finite.of_fintype Module.Basis.finTwoProd Equiv Equiv.instEquivLike of vecCons vecEmpty LinearMap.prod LinearMap.instAdd LinearMap.instSMul instDistribSMul Algebra.to_smulCommClass Algebra.id LinearMap.fst LinearMap.snd	—	LinearMap.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype Algebra.to_smulCommClass toLin_finTwoProd_apply
toLin_finTwoProd_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Prod.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instModule Semiring.toModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Matrix addCommMonoid LinearMap.addCommMonoid module LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Fin.fintype Finite.of_fintype Module.Basis.finTwoProd Equiv Equiv.instEquivLike of vecCons vecEmpty Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype toLin_apply Finset.sum_congr cons_val' cons_val_fin_one Fin.sum_univ_two Module.Basis.finTwoProd_zero mul_one MulZeroClass.mul_zero Module.Basis.finTwoProd_one add_zero zero_add
toLin_mul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap.comp RingHomCompTriple.ids Finite.of_fintype	—	LinearEquiv.injective smulCommClass_self RingHomInvPair.ids RingHomCompTriple.ids Finite.of_fintype LinearMap.toMatrix_comp LinearMap.toMatrix_toLin
toLin_mul_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype RingHomCompTriple.ids toLin_mul LinearMap.comp_apply
toLin_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne LinearMap.id	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.toMatrix_id toLin_toMatrix
toLin_pow 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Module.End.instMonoid	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype pow_zero toLin_one pow_succ RingHomCompTriple.ids toLin_mul Module.End.mul_eq_comp
toLin_scalar 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype RingHom nonAssocSemiring RingHom.instFunLike scalar LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.id	—	LinearEquiv.injective smulCommClass_self RingHomInvPair.ids Finite.of_fintype LinearMap.toMatrix_toLin map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.toMatrix_id smul_one_eq_diagonal
toLin_self 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype Module.Basis Module.Basis.instFunLike Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype toLin_apply Finset.sum_congr Module.Basis.repr_self mulVec.eq_1 dotProduct.eq_1 Finset.sum_eq_single Finsupp.single_eq_of_ne MulZeroClass.mul_zero Finset.mem_univ Finsupp.single_eq_same mul_one
toLin_symm 📖	mathematical	—	LinearEquiv.symm Matrix LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHomInvPair.ids toLin LinearMap.toMatrix	—	RingHomInvPair.ids smulCommClass_self
toLin_toMatrix 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin LinearMap.toMatrix	—	RingHomInvPair.ids smulCommClass_self toLin_symm LinearEquiv.apply_symm_apply
toLinearEquivRight'OfInv_apply 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Pi.addCommMonoid Pi.Function.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike toLinearEquivRight'OfInv LinearMap LinearMap.instFunLike MulOpposite MulOpposite.instSemiring MulOpposite.instNonAssocSemiring addCommMonoid LinearMap.addCommMonoid module Semiring.toOppositeModule LinearMap.module DFinsupp.instEquivLikeLinearEquiv toLinearMapRight'	—	RingHomInvPair.ids
toLinearEquivRight'OfInv_symm_apply 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Pi.addCommMonoid Pi.Function.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toLinearEquivRight'OfInv LinearMap LinearMap.instFunLike MulOpposite MulOpposite.instSemiring MulOpposite.instNonAssocSemiring addCommMonoid LinearMap.addCommMonoid module Semiring.toOppositeModule LinearMap.module DFinsupp.instEquivLikeLinearEquiv toLinearMapRight'	—	RingHomInvPair.ids
toLinearMapRight'_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearEquiv MulOpposite MulOpposite.instSemiring MulOpposite.instNonAssocSemiring RingHomInvPair.ids Matrix addCommMonoid LinearMap.addCommMonoid module Semiring.toOppositeModule LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsScalarTower.left EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapRight' vecMul	—	RingHomInvPair.ids Function.smulCommClass SMulCommClass.opposite_mid IsScalarTower.left
toLinearMapRight'_mul 📖	mathematical	—	DFunLike.coe LinearEquiv MulOpposite MulOpposite.instSemiring RingHom.id MulOpposite.instNonAssocSemiring Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid module Semiring.toOppositeModule LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsScalarTower.left EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapRight' instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap.comp RingHomCompTriple.ids	—	LinearMap.ext RingHomInvPair.ids Function.smulCommClass SMulCommClass.opposite_mid IsScalarTower.left RingHomCompTriple.ids vecMul_vecMul
toLinearMapRight'_mul_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearEquiv MulOpposite MulOpposite.instSemiring MulOpposite.instNonAssocSemiring RingHomInvPair.ids Matrix addCommMonoid LinearMap.addCommMonoid module Semiring.toOppositeModule LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsScalarTower.left EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapRight' instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	vecMul_vecMul
toLinearMapRight'_one 📖	mathematical	—	DFunLike.coe LinearEquiv MulOpposite MulOpposite.instSemiring RingHom.id MulOpposite.instNonAssocSemiring Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid LinearMap.addCommMonoid module Semiring.toOppositeModule LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass IsScalarTower.left EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLinearMapRight' one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne LinearMap.id	—	LinearMap.pi_ext' Finite.of_fintype RingHomInvPair.ids Function.smulCommClass SMulCommClass.opposite_mid IsScalarTower.left LinearMap.ext_ring RingHomCompTriple.ids vecMul_one
vecMulBilin_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.addCommMonoid module Pi.Function.module LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction vecMulBilin vecMul	—	Function.smulCommClass
vecMulLinear_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike vecMulLinear vecMul	—	—
vecMulLinear_transpose 📖	mathematical	—	vecMulLinear CommSemiring.toSemiring transpose mulVecLin	—	LinearMap.ext vecMul_transpose
vecMul_injective_iff 📖	mathematical	—	vecMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring LinearIndependent row Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module Semiring.toModule	—	coe_vecMulLinear linearIndependent_iff_injective_fintypeLinearCombination vecMul_eq_sum

Module.Basis

Definitions

Name	Category	Theorems
end 📖	CompOp	6 math math: end_repr_apply, end_apply_apply, end_apply, baseChange_end, LinearMap.polyCharpoly_eq_of_basis, end_repr_symm_apply
linearMap 📖	CompOp	5 math math: linearMap_apply, linearMap_repr_apply, linearMap_apply_apply, linearMap_repr_symm_apply, baseChange_linearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
end_apply 📖	mathematical	—	DFunLike.coe Module.Basis Module.End CommSemiring.toSemiring LinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike end LinearEquiv RingHomInvPair.ids Matrix LinearMap Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLin Finite.of_fintype Matrix.stdBasis	—	linearMap_apply
end_apply_apply 📖	mathematical	—	DFunLike.coe Module.End CommSemiring.toSemiring LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Module.Basis LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike end AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	linearMap_apply_apply
end_repr_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid LinearMap.module Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike repr Module.End smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction end Matrix Matrix.addCommMonoid Matrix.module Matrix.stdBasis Finite.of_fintype LinearMap.toMatrix	—	RingHomInvPair.ids smulCommClass_self
end_repr_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid LinearMap.addCommMonoid Finsupp.module Semiring.toModule LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm repr Module.End smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction end Matrix Matrix.addCommMonoid Matrix.module Matrix.toLin Finite.of_fintype LinearMap.instFunLike Finsupp.linearCombination Module.Basis instFunLike Matrix.stdBasis	—	RingHomInvPair.ids Finite.of_fintype repr_symm_apply
linearMap_apply 📖	mathematical	—	DFunLike.coe Module.Basis LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike linearMap LinearEquiv RingHomInvPair.ids Matrix Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLin Finite.of_fintype Matrix.stdBasis	—	RingHomInvPair.ids Finite.of_fintype
linearMap_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Module.Basis LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction instFunLike linearMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	smulCommClass_self RingHomInvPair.ids Finite.of_fintype linearMap_apply Matrix.stdBasis_eq_single Matrix.toLin_self Finset.sum_congr ite_smul one_smul zero_smul ite_and Finset.sum_ite_eq
linearMap_repr_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid LinearMap.module Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike repr smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction linearMap Matrix Matrix.addCommMonoid Matrix.module Matrix.stdBasis Finite.of_fintype LinearMap.toMatrix	—	RingHomInvPair.ids smulCommClass_self
linearMap_repr_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid LinearMap.addCommMonoid Finsupp.module Semiring.toModule LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm repr smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction linearMap Matrix Matrix.addCommMonoid Matrix.module Matrix.toLin Finite.of_fintype LinearMap.instFunLike Finsupp.linearCombination Module.Basis instFunLike Matrix.stdBasis	—	RingHomInvPair.ids Finite.of_fintype repr_symm_apply

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_of_surjective_fin 📖	—	DFunLike.coe Module.End Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike RingHom.id	—	—	isStablyFiniteRing_iff_injective_of_surjective

(root)

Definitions

Name	Category	Theorems
algEquivMatrix 📖	CompOp	—
algEquivMatrix' 📖	CompOp	—
dotProductBilin 📖	CompOp	1 math math: dotProductBilin_apply_apply
endVecAlgEquivMatrixEnd 📖	CompOp	2 math math: endVecAlgEquivMatrixEnd_apply_apply, endVecAlgEquivMatrixEnd_symm_apply_apply
endVecRingEquivMatrixEnd 📖	CompOp	—
matrixAlgEquivEndVecMulOpposite 📖	CompOp	—
matrixRingEquivEndVecMulOpposite 📖	CompOp	—
vecMulVecBilin 📖	CompOp	1 math math: vecMulVecBilin_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dotProductBilin_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module dotProductBilin dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
endVecAlgEquivMatrixEnd_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike AlgEquiv Module.End Pi.addCommMonoid Pi.Function.module Matrix Module.End.instSemiring Matrix.semiring Module.End.instAlgebra CommSemiring.toSemiring Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' Algebra.toSMul Pi.isScalarTower Matrix.instAlgebra AlgEquiv.instFunLike endVecAlgEquivMatrixEnd Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	Function.smulCommClass IsScalarTower.to_smulCommClass' Pi.isScalarTower
endVecAlgEquivMatrixEnd_symm_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Pi.Function.module LinearMap.instFunLike AlgEquiv Matrix Module.End Matrix.semiring Module.End.instSemiring Matrix.instAlgebra Module.End.instAlgebra IsScalarTower.to_smulCommClass' Algebra.toSMul CommSemiring.toSemiring Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Pi.isScalarTower AlgEquiv.instFunLike AlgEquiv.symm endVecAlgEquivMatrixEnd Finset.sum Finset.univ	—	IsScalarTower.to_smulCommClass' Function.smulCommClass Pi.isScalarTower
instIsStablyFiniteRingEndForallOfFinite 📖	mathematical	—	IsStablyFiniteRing Module.End Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring LinearMap.addCommMonoid RingHom.id	—	MulOpposite.isStablyFiniteRing_iff RingEquiv.isStablyFiniteRing_iff RingEquiv.instRingEquivClass Matrix.instIsStablyFiniteRing
isStablyFiniteRing_iff_injective_of_surjective 📖	mathematical	—	IsStablyFiniteRing MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring DFunLike.coe Module.End Pi.addCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike RingHom.id	—	RingHomCompTriple.ids Module.projective_lifting_property Module.Projective.of_free Module.Free.function Finite.of_fintype Module.Free.self LinearMap.injective_of_comp_eq_id RingHomInvPair.ids LinearMap.surjective_of_comp_eq_id RingHomInvPair.triples₂ LinearEquiv.symm_comp left_inv_eq_right_inv
isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd 📖	mathematical	—	IsStablyFiniteRing MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsDedekindFiniteMonoid Module.End Pi.addCommMonoid Pi.Function.module Semiring.toModule Module.End.instSemiring	—	MulEquivClass.isDedekindFiniteMonoid_iff RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass
range_vecMulLinear 📖	mathematical	—	LinearMap.range Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id RingHomSurjective.ids Matrix.vecMulLinear Submodule.span Set.range Matrix.row	—	RingHomSurjective.ids LinearMap.range_eq_map Submodule.map.congr_simp Finite.of_fintype Submodule.map_iSup Submodule.map_span Set.image_image Set.image_singleton Submodule.iSup_span Set.range_eq_iUnion Set.iUnion_singleton_eq_range single_dotProduct one_mul
toMatrix_distrib_mul_action_toLinearMap 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Finite.of_fintype DistribSMul.toLinearMap DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.toMatrix_apply DistribSMul.toLinearMap_apply map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Module.Basis.repr_self Finsupp.smul_single_one Finsupp.single_eq_pi_single Matrix.diagonal_apply Pi.single_apply
vecMulVecBilin_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Matrix Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.addCommMonoid Pi.Function.module Matrix.module LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Matrix.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction vecMulVecBilin Matrix.vecMulVec Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Matrix.smulCommClass

---

← Back to Index