Documentation Verification Report

MatrixAlgebra

📁 Source: Mathlib/RingTheory/MatrixAlgebra.lean

Statistics

Metric	Count
Definitions `kroneckerAlgEquiv`, `kroneckerStarAlgEquiv`, `kroneckerTMulAlgEquiv`, `kroneckerTMulStarAlgEquiv`, `equiv`, `invFun`, `toFunAlgHom`, `toFunBilinear`, `toFunLinear`, `kroneckerLinearEquiv`, `kroneckerTMulLinearEquiv`, `matrixEquivTensor`	12
Theorems `kroneckerAlgEquiv_apply`, `kroneckerAlgEquiv_symm_apply`, `kroneckerStarAlgEquiv_apply`, `kroneckerStarAlgEquiv_symm_apply`, `kroneckerTMulAlgEquiv_apply`, `kroneckerTMulAlgEquiv_symm_apply`, `kroneckerTMulStarAlgEquiv_apply`, `kroneckerTMulStarAlgEquiv_symm_apply`, `toAlgEquiv_kroneckerStarAlgEquiv`, `toAlgEquiv_kroneckerTMulStarAlgEquiv`, `toLinearEquiv_kroneckerAlgEquiv`, `invFun_add`, `invFun_algebraMap`, `invFun_smul`, `invFun_zero`, `left_inv`, `right_inv`, `toFunAlgHom_apply`, `toFunBilinear_apply`, `kroneckerLinearEquiv_symm_kronecker`, `kroneckerLinearEquiv_tmul`, `kroneckerTMulAlgEquiv_symm_single_tmul`, `kroneckerTMulLinearEquiv_mul`, `kroneckerTMulLinearEquiv_one`, `kroneckerTMulLinearEquiv_symm_kroneckerTMul`, `kroneckerTMulLinearEquiv_tmul`, `matrixEquivTensor_apply`, `matrixEquivTensor_apply_single`, `matrixEquivTensor_apply_symm`	29
Total	41

Matrix

Definitions

Name	Category	Theorems
`kroneckerAlgEquiv` 📖	CompOp	4 math math: `toAlgEquiv_kroneckerStarAlgEquiv`, `kroneckerAlgEquiv_apply`, `kroneckerAlgEquiv_symm_apply`, `toLinearEquiv_kroneckerAlgEquiv`
`kroneckerStarAlgEquiv` 📖	CompOp	3 math math: `toAlgEquiv_kroneckerStarAlgEquiv`, `kroneckerStarAlgEquiv_apply`, `kroneckerStarAlgEquiv_symm_apply`
`kroneckerTMulAlgEquiv` 📖	CompOp	3 math math: `toAlgEquiv_kroneckerTMulStarAlgEquiv`, `kroneckerTMulAlgEquiv_symm_apply`, `kroneckerTMulAlgEquiv_apply`
`kroneckerTMulStarAlgEquiv` 📖	CompOp	3 math math: `kroneckerTMulStarAlgEquiv_symm_apply`, `toAlgEquiv_kroneckerTMulStarAlgEquiv`, `kroneckerTMulStarAlgEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`kroneckerAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `semiring` `instAlgebra` `Algebra.id` `instFintypeProd` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `kroneckerAlgEquiv` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `kroneckerLinearEquiv`	—	—
`kroneckerAlgEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `TensorProduct` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `module` `Semiring.toModule` `semiring` `instFintypeProd` `Algebra.TensorProduct.instSemiring` `instAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `kroneckerAlgEquiv` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `kroneckerLinearEquiv`	—	—
`kroneckerStarAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `TensorProduct` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `module` `Semiring.toModule` `TensorProduct.add` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Algebra.TensorProduct.instMul` `nonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `semiring` `instAlgebra` `Algebra.id` `IsScalarTower.right` `instMulOfFintypeOfAddCommMonoid` `instFintypeProd` `Distrib.toMul` `TensorProduct.instSMul` `smul` `Algebra.toSMul` `TensorProduct.instStar` `instStarAddMonoid` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `Module.toDistribMulAction` `StarMul.toStarModule` `CommSemiring.toCommMonoid` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instStar` `StarAlgEquiv.instFunLike` `kroneckerStarAlgEquiv` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `kroneckerLinearEquiv`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `instStarModule` `StarMul.toStarModule`
`kroneckerStarAlgEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `Matrix` `TensorProduct` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `module` `Semiring.toModule` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `TensorProduct.add` `instMulOfFintypeOfAddCommMonoid` `instFintypeProd` `Distrib.toMul` `Algebra.TensorProduct.instMul` `nonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `semiring` `instAlgebra` `Algebra.id` `IsScalarTower.right` `smul` `Algebra.toSMul` `TensorProduct.instSMul` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `TensorProduct.instStar` `instStarAddMonoid` `instStarModule` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `Module.toDistribMulAction` `StarMul.toStarModule` `CommSemiring.toCommMonoid` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `StarAlgEquiv.instFunLike` `StarAlgEquiv.symm` `kroneckerStarAlgEquiv` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `kroneckerLinearEquiv`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `instStarModule` `StarMul.toStarModule`
`kroneckerTMulAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `module` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `semiring` `instAlgebra` `instFintypeProd` `Algebra.TensorProduct.leftAlgebra` `smulCommClass` `Algebra.toSMul` `IsScalarTower.to_smulCommClass` `AlgEquiv.instFunLike` `kroneckerTMulAlgEquiv` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `kroneckerTMulLinearEquiv`	—	`smulCommClass` `IsScalarTower.to_smulCommClass`
`kroneckerTMulAlgEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `addCommMonoid` `module` `CommSemiring.toSemiring` `semiring` `Algebra.TensorProduct.instSemiring` `instFintypeProd` `instAlgebra` `Algebra.TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `smulCommClass` `Algebra.toSMul` `AlgEquiv.instFunLike` `AlgEquiv.symm` `kroneckerTMulAlgEquiv` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `kroneckerTMulLinearEquiv`	—	`IsScalarTower.to_smulCommClass` `smulCommClass`
`kroneckerTMulStarAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `TensorProduct` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `module` `CommSemiring.toSemiring` `Algebra.toModule` `TensorProduct.add` `add` `Algebra.TensorProduct.instMul` `nonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `semiring` `instAlgebra` `IsScalarTower.right` `instMulOfFintypeOfAddCommMonoid` `instFintypeProd` `TensorProduct.addCommMonoid` `TensorProduct.leftHasSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `distribMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `IsScalarTower.to_smulCommClass` `smul` `TensorProduct.instStar` `instStarAddMonoid` `instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `instStar` `StarAlgEquiv.instFunLike` `kroneckerTMulStarAlgEquiv` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.leftModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `kroneckerTMulLinearEquiv`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `smulCommClass` `IsScalarTower.to_smulCommClass` `instStarModule`
`kroneckerTMulStarAlgEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `Matrix` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `addCommMonoid` `module` `CommSemiring.toSemiring` `add` `TensorProduct.add` `instMulOfFintypeOfAddCommMonoid` `instFintypeProd` `Algebra.TensorProduct.instMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `TensorProduct.addCommMonoid` `nonUnitalNonAssocSemiring` `semiring` `instAlgebra` `smul` `TensorProduct.leftHasSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass` `distribMulAction` `AddCommMonoid.toAddMonoid` `smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `instStar` `TensorProduct.instStar` `instStarAddMonoid` `instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `StarAlgEquiv.instFunLike` `StarAlgEquiv.symm` `kroneckerTMulStarAlgEquiv` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `TensorProduct.leftModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `kroneckerTMulLinearEquiv`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `IsScalarTower.to_smulCommClass` `smulCommClass` `instStarModule`
`toAlgEquiv_kroneckerStarAlgEquiv` 📖	mathematical	—	`StarAlgEquiv.toAlgEquiv` `TensorProduct` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `semiring` `instAlgebra` `Algebra.id` `instFintypeProd` `Algebra.TensorProduct.instAlgebra` `TensorProduct.instStar` `instStarAddMonoid` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `Module.toDistribMulAction` `StarMul.toStarModule` `CommSemiring.toCommMonoid` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instStar` `kroneckerStarAlgEquiv` `kroneckerAlgEquiv`	—	`instStarModule` `StarMul.toStarModule`
`toAlgEquiv_kroneckerTMulStarAlgEquiv` 📖	mathematical	—	`StarAlgEquiv.toAlgEquiv` `TensorProduct` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `module` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instSemiring` `semiring` `instAlgebra` `instFintypeProd` `Algebra.TensorProduct.leftAlgebra` `smulCommClass` `Algebra.toSMul` `IsScalarTower.to_smulCommClass` `TensorProduct.instStar` `instStarAddMonoid` `AddCommMonoid.toAddMonoid` `instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `Module.toDistribMulAction` `instStar` `kroneckerTMulStarAlgEquiv` `kroneckerTMulAlgEquiv`	—	`smulCommClass` `IsScalarTower.to_smulCommClass` `instStarModule`
`toLinearEquiv_kroneckerAlgEquiv` 📖	mathematical	—	`AlgEquiv.toLinearEquiv` `TensorProduct` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `semiring` `instAlgebra` `Algebra.id` `instFintypeProd` `Algebra.TensorProduct.instAlgebra` `kroneckerAlgEquiv` `kroneckerLinearEquiv`	—	`RingHomInvPair.ids`

MatrixEquivTensor

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	—
`invFun` 📖	CompOp	6 math math: `invFun_add`, `invFun_algebraMap`, `invFun_smul`, `left_inv`, `right_inv`, `invFun_zero`
`toFunAlgHom` 📖	CompOp	3 math math: `left_inv`, `right_inv`, `toFunAlgHom_apply`
`toFunBilinear` 📖	CompOp	1 math math: `toFunBilinear_apply`
`toFunLinear` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`invFun_add` 📖	mathematical	—	`invFun` `Matrix` `Matrix.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Matrix.module` `Semiring.toModule` `TensorProduct.add`	—	`Finset.sum_congr` `TensorProduct.add_tmul` `Finset.sum_add_distrib`
`invFun_algebraMap` 📖	mathematical	—	`invFun` `Matrix.map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `TensorProduct.tmul` `Matrix` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix.addCommMonoid` `Algebra.toModule` `Matrix.module` `Semiring.toModule` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finset.sum_congr` `Algebra.algebraMap_eq_smul_one` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `Matrix.isScalarTower` `IsScalarTower.right` `Matrix.matrix_eq_sum_single` `Matrix.smul_single` `mul_one` `Finset.sum_product`
`invFun_smul` 📖	mathematical	—	`invFun` `Matrix` `Matrix.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Matrix.module` `Semiring.toModule` `Algebra.TensorProduct.instMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `Matrix.nonUnitalNonAssocSemiring` `Matrix.semiring` `Matrix.instAlgebra` `Algebra.id` `TensorProduct.tmul` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `Finset.sum_congr` `Finset.mul_sum` `one_mul`
`invFun_zero` 📖	mathematical	—	`invFun` `Matrix` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Matrix.module` `Semiring.toModule` `TensorProduct.zero`	—	`Finset.sum_congr` `TensorProduct.zero_tmul` `Finset.sum_const_zero`
`left_inv` 📖	mathematical	—	`invFun` `DFunLike.coe` `AlgHom` `TensorProduct` `Matrix` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Matrix.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Matrix.semiring` `Matrix.instAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `toFunAlgHom`	—	`TensorProduct.induction_on` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `Algebra.to_smulCommClass` `IsScalarTower.right` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `invFun_zero` `invFun_smul` `invFun_algebraMap` `mul_one` `one_mul` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `invFun_add`
`right_inv` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorProduct` `Matrix` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Matrix.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Matrix.semiring` `Matrix.instAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `toFunAlgHom` `invFun`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Finset.sum_congr` `Matrix.matrix_eq_sum_single` `Matrix.ext` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MulZeroClass.mul_zero` `Finset.sum_product`
`toFunAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorProduct` `Matrix` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Matrix.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Matrix.semiring` `Matrix.instAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `toFunAlgHom` `TensorProduct.tmul` `Matrix.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `Matrix.map` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—
`toFunBilinear_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix.module` `Semiring.toModule` `Algebra.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Matrix.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `CommMonoid.toMonoid` `toFunBilinear` `Matrix.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `Matrix.map` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Matrix.smulCommClass` `smulCommClass_self`

(root)

Definitions

Name	Category	Theorems
`kroneckerLinearEquiv` 📖	CompOp	7 math math: `Matrix.kroneckerAlgEquiv_apply`, `kroneckerLinearEquiv_symm_kronecker`, `Matrix.kroneckerAlgEquiv_symm_apply`, `Matrix.toLinearEquiv_kroneckerAlgEquiv`, `Matrix.kroneckerStarAlgEquiv_apply`, `Matrix.kroneckerStarAlgEquiv_symm_apply`, `kroneckerLinearEquiv_tmul`
`kroneckerTMulLinearEquiv` 📖	CompOp	9 math math: `Matrix.kroneckerTMulStarAlgEquiv_symm_apply`, `kroneckerTMulAlgEquiv_symm_single_tmul`, `kroneckerTMulLinearEquiv_one`, `Matrix.kroneckerTMulAlgEquiv_symm_apply`, `Matrix.kroneckerTMulStarAlgEquiv_apply`, `kroneckerTMulLinearEquiv_mul`, `kroneckerTMulLinearEquiv_symm_kroneckerTMul`, `kroneckerTMulLinearEquiv_tmul`, `Matrix.kroneckerTMulAlgEquiv_apply`
`matrixEquivTensor` 📖	CompOp	3 math math: `matrixEquivTensor_apply_single`, `matrixEquivTensor_apply_symm`, `matrixEquivTensor_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`kroneckerLinearEquiv_symm_kronecker` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `TensorProduct` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix.module` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `kroneckerLinearEquiv` `Matrix.kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `TensorProduct.tmul`	—	`RingHomInvPair.ids`
`kroneckerLinearEquiv_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix.module` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `kroneckerLinearEquiv` `TensorProduct.tmul` `Matrix.kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`RingHomInvPair.ids`
`kroneckerTMulAlgEquiv_symm_single_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `TensorProduct` `Matrix.addCommMonoid` `Matrix.module` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `Matrix.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `kroneckerTMulLinearEquiv` `Matrix.single` `TensorProduct.zero` `TensorProduct.tmul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `Matrix.smulCommClass` `LinearEquiv.symm_apply_eq` `kroneckerTMulLinearEquiv_tmul` `Matrix.single_kroneckerTMul_single`
`kroneckerTMulLinearEquiv_mul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix.module` `CommSemiring.toSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Matrix.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `kroneckerTMulLinearEquiv` `Algebra.TensorProduct.instMul` `Matrix.nonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Matrix.semiring` `Matrix.instAlgebra` `IsScalarTower.right` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `instFintypeProd`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `Matrix.smulCommClass` `IsScalarTower.to_smulCommClass` `LinearMap.IsScalarTower.compatibleSMul` `TensorProduct.isScalarTower_left` `Matrix.isScalarTower` `RingHomInvPair.ids` `smulCommClass_self` `IsScalarTower.left` `RingHomCompTriple.ids` `LinearMap.map_mul_iff` `TensorProduct.AlgebraTensorModule.curry_injective` `TensorProduct.smulCommClass_left` `LinearMap.instIsScalarTower` `TensorProduct.isScalarTower` `Matrix.ext_linearMap` `Finite.of_fintype` `LinearMap.ext` `Matrix.mul_kroneckerTMul_mul` `Matrix.single_kroneckerTMul_single`
`kroneckerTMulLinearEquiv_one` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `Matrix` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix.module` `CommSemiring.toSemiring` `Algebra.toModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Matrix.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `kroneckerTMulLinearEquiv` `Algebra.TensorProduct.instOneTensorProduct` `Matrix.instAddCommMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Matrix.one` `TensorProduct.zero`	—	`RingHomInvPair.ids` `Matrix.smulCommClass` `IsScalarTower.to_smulCommClass` `Matrix.kroneckerMap_one_one` `TensorProduct.zero_tmul` `TensorProduct.tmul_zero`
`kroneckerTMulLinearEquiv_symm_kroneckerTMul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `TensorProduct` `Matrix.addCommMonoid` `Matrix.module` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `Matrix.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `kroneckerTMulLinearEquiv` `Matrix.kroneckerMap` `TensorProduct.tmul`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass` `Matrix.smulCommClass`
`kroneckerTMulLinearEquiv_tmul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `TensorProduct` `Matrix` `Matrix.addCommMonoid` `Matrix.module` `CommSemiring.toSemiring` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `Matrix.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `kroneckerTMulLinearEquiv` `TensorProduct.tmul` `Matrix.kroneckerMap`	—	`RingHomInvPair.ids` `Matrix.smulCommClass` `IsScalarTower.to_smulCommClass`
`matrixEquivTensor_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Matrix.module` `Semiring.toModule` `Matrix.semiring` `Algebra.TensorProduct.instSemiring` `Matrix.instAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `matrixEquivTensor` `Finset.sum` `TensorProduct.addCommMonoid` `Finset.univ` `instFintypeProd` `TensorProduct.tmul` `Matrix.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`matrixEquivTensor_apply_single` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Matrix` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Matrix.module` `Semiring.toModule` `Matrix.semiring` `Algebra.TensorProduct.instSemiring` `Matrix.instAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `matrixEquivTensor` `Matrix.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Finset.sum_congr` `TensorProduct.ite_tmul` `Finset.sum_ite_eq'`
`matrixEquivTensor_apply_symm` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `Matrix` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Matrix.addCommMonoid` `CommSemiring.toSemiring` `Algebra.toModule` `Matrix.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Matrix.semiring` `Matrix.instAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `matrixEquivTensor` `TensorProduct.tmul` `Matrix.smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `Matrix.map` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—

---

← Back to Index