Basis

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

Statistics

Metric	Count
Definitions invertibleToMatrix, toMatrix, toMatrixEquiv	3
Theorems toMatrix_id_eq_basis_toMatrix, toMatrix_eq_transpose, restrictScalars_toMatrix, sum_toMatrix_smul_self, toLin_toMatrix, toMatrix_apply, toMatrix_eq_toMatrix_constr, toMatrix_isUnitSMul, toMatrix_map, toMatrix_map_vecMul, toMatrix_mulVec_repr, toMatrix_mul_toMatrix, toMatrix_mul_toMatrix_flip, toMatrix_reindex, toMatrix_reindex', toMatrix_self, toMatrix_smul, toMatrix_smul_left, toMatrix_transpose_apply, toMatrix_unitsSMul, toMatrix_update, basis_toMatrix_basisFun_mul, basis_toMatrix_mul, basis_toMatrix_mul_linearMap_toMatrix, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, linearMap_toMatrix_mul_basis_toMatrix, mul_basis_toMatrix	27
Total	30

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMatrix_id_eq_basis_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 id Module.Basis.toMatrix Module.Basis Module.Basis.instFunLike	—	Matrix.ext RingHomInvPair.ids smulCommClass_self toMatrix_apply

Module.Basis

Definitions

Name	Category	Theorems
invertibleToMatrix 📖	CompOp	—
toMatrix 📖	CompOp	41 math math: toMatrix_smul, LDL.lowerInv_eq_gramSchmidtBasis, toLin_toMatrix, toMatrix_map, basis_toMatrix_basisFun_mul, linearMap_toMatrix_mul_basis_toMatrix, mul_basis_toMatrix, PowerBasis.toMatrix_isIntegral, sum_toMatrix_smul_self, BilinForm.toMatrix_mul_basis_toMatrix, toMatrix_apply, continuous_toMatrix, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangular, Matrix.IsHermitian.eigenvectorUnitary_coe, coePiBasisFun.toMatrix_eq_transpose, toMatrix_mul_toMatrix_flip, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix, toMatrix_update, PiLp.basis_toMatrix_basisFun_mul, LinearMap.toMatrix₂_mul_basis_toMatrix, toMatrix_eq_toMatrix_constr, OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary, toMatrix_isUnitSMul, toMatrix_reindex, toMatrix_smul_left, toMatrix_transpose_apply, OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, toMatrix_reindex', OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self, OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal, basis_toMatrix_mul_linearMap_toMatrix, toMatrix_self, basis_toMatrix_mul, toMatrix_mul_toMatrix, toMatrix_mulVec_repr, toMatrix_unitsSMul, toMatrix_map_vecMul, det_apply, restrictScalars_toMatrix, LinearMap.toMatrix_id_eq_basis_toMatrix
toMatrixEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictScalars_toMatrix 📖	mathematical	—	DFunLike.coe RingHom Matrix Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.mapMatrix algebraMap toMatrix Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range Module.Basis Ring.toSemiring CommRing.toRing instFunLike Submodule.addCommMonoid Submodule.module restrictScalars	—	Matrix.ext RingHom.mapMatrix_apply Matrix.map_apply RingHomInvPair.ids toMatrix_apply restrictScalars_repr_apply
sum_toMatrix_smul_self 📖	mathematical	—	Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction toMatrix DFunLike.coe Module.Basis instFunLike	—	RingHomInvPair.ids Finset.sum_congr toMatrix_apply sum_repr
toLin_toMatrix 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid Matrix.module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLin toMatrix Module.Basis instFunLike LinearMap.id	—	ext RingHomInvPair.ids smulCommClass_self nonempty_fintype Finite.of_fintype Matrix.toLin_self LinearMap.id_apply sum_toMatrix_smul_self
toMatrix_apply 📖	mathematical	—	toMatrix 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 repr	—	—
toMatrix_eq_toMatrix_constr 📖	mathematical	—	toMatrix 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 Nat.instSemiring Pi.addCommMonoid Pi.Function.module AddCommMonoid.toNatModule AddMonoid.nat_smulCommClass' DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero constr	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype AddMonoid.nat_smulCommClass' toMatrix_apply LinearMap.toMatrix_apply constr_basis
toMatrix_isUnitSMul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	toMatrix AddCommGroup.toAddCommMonoid DFunLike.coe Module.Basis instFunLike isUnitSMul Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	toMatrix_unitsSMul
toMatrix_map 📖	mathematical	—	toMatrix map CommSemiring.toSemiring DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm	—	RingHomInvPair.ids Matrix.ext
toMatrix_map_vecMul 📖	mathematical	—	Matrix.vecMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe Module.Basis CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule instFunLike Matrix.map toMatrix RingHom RingHom.instFunLike algebraMap	—	Finset.sum_congr sum_toMatrix_smul_self
toMatrix_mulVec_repr 📖	mathematical	—	Matrix.mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring toMatrix DFunLike.coe Module.Basis instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv repr	—	nonempty_fintype RingHomInvPair.ids smulCommClass_self LinearMap.toMatrix_mulVec_repr
toMatrix_mul_toMatrix 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix DFunLike.coe Module.Basis instFunLike	—	Matrix.ext RingHomInvPair.ids Finset.sum_congr sum_repr_mul_repr
toMatrix_mul_toMatrix_flip 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix DFunLike.coe Module.Basis instFunLike Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toMatrix_mul_toMatrix toMatrix_self
toMatrix_reindex 📖	mathematical	—	toMatrix reindex CommSemiring.toSemiring Matrix.submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	Matrix.ext RingHomInvPair.ids repr_reindex Finsupp.mapDomain_equiv_apply
toMatrix_reindex' 📖	mathematical	—	toMatrix reindex CommSemiring.toSemiring DFunLike.coe AlgEquiv Matrix Matrix.semiring Matrix.instAlgebra Algebra.id AlgEquiv.instFunLike Matrix.reindexAlgEquiv Equiv EquivLike.toFunLike Equiv.instEquivLike	—	Matrix.ext RingHomInvPair.ids repr_reindex Finsupp.mapDomain_equiv_apply Equiv.apply_symm_apply
toMatrix_self 📖	mathematical	—	toMatrix DFunLike.coe Module.Basis CommSemiring.toSemiring instFunLike Matrix Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Matrix.ext repr_self Finsupp.single_apply
toMatrix_smul 📖	mathematical	—	toMatrix NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib CommSemiring.toSemiring DFunLike.coe AlgHom Matrix.semiring Matrix.instAlgebra Algebra.id AlgHom.funLike Algebra.leftMulMatrix	—	Matrix.ext RingHomInvPair.ids toMatrix_apply Pi.smul_apply smul_eq_mul Algebra.leftMulMatrix_mulVec_repr
toMatrix_smul_left 📖	mathematical	—	toMatrix Module.Basis CommSemiring.toSemiring instSMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
toMatrix_transpose_apply 📖	mathematical	—	Matrix.transpose toMatrix 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 repr	—	RingHomInvPair.ids
toMatrix_unitsSMul 📖	mathematical	—	toMatrix CommRing.toCommSemiring AddCommGroup.toAddCommMonoid DFunLike.coe Module.Basis CommSemiring.toSemiring instFunLike unitsSMul Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units.val	—	Matrix.ext RingHomInvPair.ids unitsSMul_apply map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass repr_self Finsupp.smul_single mul_one Finsupp.single_eq_same Matrix.diagonal.congr_simp Matrix.diagonal_apply_eq Finsupp.single_eq_of_ne Matrix.diagonal_apply_ne
toMatrix_update 📖	mathematical	—	toMatrix Function.update Matrix.updateCol 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 repr	—	Matrix.ext RingHomInvPair.ids toMatrix.eq_1 Matrix.updateCol_apply toMatrix_apply Function.update_self Function.update_of_ne

Module.Basis.coePiBasisFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMatrix_eq_transpose 📖	mathematical	—	Module.Basis.toMatrix Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.Function.module Semiring.toModule Pi.basisFun Matrix.transpose	—	Matrix.ext

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_toMatrix_basisFun_mul 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Module.Basis.toMatrix Pi.addCommMonoid Pi.Function.module Semiring.toModule DFunLike.coe Module.Basis Module.Basis.instFunLike Pi.basisFun Finite.of_fintype Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Matrix.col	—	Finite.of_fintype RingHomInvPair.ids smulCommClass_self basis_toMatrix_mul Matrix.ext LinearMap.toMatrix_apply Function.smulCommClass Algebra.to_smulCommClass Matrix.toLin'_apply Pi.basisFun_apply Matrix.mulVec_single_one Matrix.of_apply
basis_toMatrix_mul 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Module.Basis.toMatrix DFunLike.coe Module.Basis Module.Basis.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids LinearMap 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 Matrix.toLin Finite.of_fintype	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype basis_toMatrix_mul_linearMap_toMatrix LinearMap.toMatrix_toLin
basis_toMatrix_mul_linearMap_toMatrix 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Module.Basis.toMatrix DFunLike.coe Module.Basis Module.Basis.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids LinearMap 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	—	LinearEquiv.injective smulCommClass_self RingHomInvPair.ids Finite.of_fintype Matrix.toLin_toMatrix RingHomCompTriple.ids Matrix.toLin_mul Module.Basis.toLin_toMatrix RingHomCompTriple.right_ids LinearMap.id_comp
basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Module.Basis.toMatrix DFunLike.coe Module.Basis Module.Basis.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids LinearMap 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	—	nonempty_fintype RingHomInvPair.ids smulCommClass_self Finite.of_fintype basis_toMatrix_mul_linearMap_toMatrix linearMap_toMatrix_mul_basis_toMatrix
linearMap_toMatrix_mul_basis_toMatrix 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap 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 Module.Basis.toMatrix Module.Basis Module.Basis.instFunLike	—	LinearEquiv.injective smulCommClass_self RingHomInvPair.ids Matrix.toLin_toMatrix RingHomCompTriple.ids Finite.of_fintype Matrix.toLin_mul Module.Basis.toLin_toMatrix LinearMap.comp_id
mul_basis_toMatrix 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Module.Basis.toMatrix DFunLike.coe Module.Basis Module.Basis.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids LinearMap 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 Matrix.toLin	—	nonempty_fintype RingHomInvPair.ids smulCommClass_self linearMap_toMatrix_mul_basis_toMatrix LinearMap.toMatrix_toLin

---

← Back to Index