Matrix

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

Statistics

Metric	Count
Definitions	0
Theorems toLin_kronecker, toMatrix_assoc, toMatrix_comm, toMatrix_map	4
Total	4

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLin_kronecker 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap TensorProduct AddCommGroup.toAddCommMonoid TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin instFintypeProd Finite.instProd Module.Basis.tensorProduct kroneckerMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TensorProduct.map	—	IsScalarTower.to_smulCommClass IsScalarTower.left RingHomInvPair.ids smulCommClass_self Finite.instProd LinearEquiv.eq_symm_apply toLin_symm TensorProduct.toMatrix_map LinearMap.toMatrix_toLin

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMatrix_assoc 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap TensorProduct AddCommGroup.toAddCommMonoid addCommMonoid instModule leftModule IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction isScalarTower Algebra.toSMul Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix instFintypeProd Finite.instProd Finite.of_fintype Module.Basis.tensorProduct LinearEquiv.toLinearMap assoc Matrix.submatrix Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Equiv Equiv.instEquivLike Equiv.prodAssoc	—	Matrix.ext RingHomInvPair.ids IsScalarTower.to_smulCommClass IsScalarTower.left isScalarTower smulCommClass_self Finite.instProd Finite.of_fintype LinearMap.toMatrix_apply Module.Basis.tensorProduct_apply Module.Basis.tensorProduct_repr_tmul_apply Module.Basis.repr_self Finsupp.single_apply mul_ite mul_one MulZeroClass.mul_zero
toMatrix_comm 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap TensorProduct AddCommGroup.toAddCommMonoid addCommMonoid leftModule IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix instFintypeProd Finite.instProd Finite.of_fintype Module.Basis.tensorProduct LinearEquiv.toLinearMap instModule comm Matrix.submatrix Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.ext RingHomInvPair.ids IsScalarTower.to_smulCommClass IsScalarTower.left smulCommClass_self Finite.instProd Finite.of_fintype LinearMap.toMatrix_apply Module.Basis.tensorProduct_apply Module.Basis.tensorProduct_repr_tmul_apply Module.Basis.repr_self Finsupp.single_apply mul_ite mul_one MulZeroClass.mul_zero
toMatrix_map 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap TensorProduct AddCommGroup.toAddCommMonoid addCommMonoid leftModule IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix LinearMap.addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix instFintypeProd Finite.instProd Module.Basis.tensorProduct map Matrix.kroneckerMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Matrix.ext RingHomInvPair.ids IsScalarTower.to_smulCommClass IsScalarTower.left smulCommClass_self Finite.instProd LinearMap.toMatrix_apply Module.Basis.tensorProduct_apply Module.Basis.tensorProduct_repr_tmul_apply mul_comm

---

← Back to Index