Kronecker

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

Statistics

Metric	Count
Definitions `«term_⊗ₖ_»`, `«term_⊗ₖₜ[_]_»`, `«term_⊗ₖₜ_»`, `kronecker`, `kroneckerBilinear`, `kroneckerMap`, `kroneckerMapBilinear`, `kroneckerTMul`, `kroneckerTMulBilinear`	9
Theorems `add_kronecker`, `add_kroneckerTMul`, `conjTranspose_kronecker`, `conjTranspose_kronecker'`, `conjTranspose_kroneckerTMul`, `det_kronecker`, `det_kroneckerMapBilinear`, `det_kroneckerTMul`, `diagonal_kronecker`, `diagonal_kroneckerTMul`, `diagonal_kroneckerTMul_diagonal`, `diagonal_kronecker_diagonal`, `kroneckerMapBilinear_apply_apply`, `kroneckerMapBilinear_mul_mul`, `kroneckerMap_add_left`, `kroneckerMap_add_right`, `kroneckerMap_apply`, `kroneckerMap_assoc`, `kroneckerMap_assoc₁`, `kroneckerMap_diagonal_diagonal`, `kroneckerMap_diagonal_left`, `kroneckerMap_diagonal_right`, `kroneckerMap_map`, `kroneckerMap_map_left`, `kroneckerMap_map_right`, `kroneckerMap_one_one`, `kroneckerMap_reindex`, `kroneckerMap_reindex_left`, `kroneckerMap_reindex_right`, `kroneckerMap_single_single`, `kroneckerMap_smul_left`, `kroneckerMap_smul_right`, `kroneckerMap_transpose`, `kroneckerMap_zero_left`, `kroneckerMap_zero_right`, `kroneckerTMulBilinear_apply`, `kroneckerTMul_add`, `kroneckerTMul_apply`, `kroneckerTMul_assoc`, `kroneckerTMul_assoc'`, `kroneckerTMul_diagonal`, `kroneckerTMul_smul`, `kroneckerTMul_zero`, `kronecker_add`, `kronecker_apply`, `kronecker_assoc`, `kronecker_assoc'`, `kronecker_diagonal`, `kronecker_natCast`, `kronecker_ofNat`, `kronecker_one`, `kronecker_smul`, `kronecker_zero`, `mul_kroneckerTMul_mul`, `mul_kronecker_mul`, `natCast_kronecker`, `natCast_kronecker_natCast`, `ofNat_kronecker`, `one_kronecker`, `one_kroneckerTMul_one`, `one_kronecker_one`, `single_kroneckerTMul_single`, `single_kronecker_single`, `smul_kronecker`, `smul_kroneckerTMul`, `trace_kronecker`, `trace_kroneckerMapBilinear`, `trace_kroneckerTMul`, `zero_kronecker`, `zero_kroneckerTMul`	70
Total	79

Kronecker

Definitions

Name	Category	Theorems
`«term_⊗ₖ_»` 📖	CompOp	—
`«term_⊗ₖₜ[_]_»` 📖	CompOp	—
`«term_⊗ₖₜ_»` 📖	CompOp	—

Matrix

Definitions

Name	Category	Theorems
`kronecker` 📖	CompOp	—
`kroneckerBilinear` 📖	CompOp	—
`kroneckerMap` 📖	CompOp	85 math math: `natCast_kronecker`, `toLin_kronecker`, `kronecker_natCast`, `kroneckerMap_map_left`, `one_kronecker`, `kronecker_add`, `kroneckerTMul_zero`, `trace_kronecker`, `kroneckerMap_reindex_right`, `kroneckerTMul_assoc'`, `kroneckerMap_assoc₁`, `kroneckerMap_reindex`, `zero_kronecker`, `add_kronecker`, `conjTranspose_kronecker`, `kroneckerMap_map_right`, `kroneckerMap_one_one`, `smul_kroneckerTMul`, `kroneckerMap_diagonal_right`, `mul_kronecker_mul`, `kroneckerMapBilinear_apply_apply`, `det_kronecker`, `IsUnit.kronecker`, `kroneckerMap_reindex_left`, `single_kroneckerTMul_single`, `single_kronecker_single`, `kroneckerLinearEquiv_symm_kronecker`, `conjTranspose_kroneckerTMul`, `diagonal_kroneckerTMul_diagonal`, `diagonal_kroneckerTMul`, `kroneckerMap_apply`, `kroneckerTMulLinearEquiv_symm_kroneckerTMul`, `kronecker_mem_unitary`, `kroneckerTMulLinearEquiv_tmul`, `kroneckerTMul_add`, `PosSemidef.kronecker`, `kronecker_assoc`, `vec_vecMul_kronecker_of_commute`, `kronecker_assoc'`, `kronecker_one`, `kroneckerMap_single_single`, `kroneckerMap_map`, `smul_kronecker`, `kronecker_ofNat`, `one_kronecker_one`, `kroneckerMap_smul_left`, `inv_kronecker`, `diagonal_kronecker`, `add_kroneckerTMul`, `vec_vecMul_kronecker`, `kronecker_apply`, `PosDef.kronecker`, `kronecker_mulVec_vec`, `kroneckerTMul_smul`, `kroneckerMap_assoc`, `kroneckerMap_diagonal_diagonal`, `kroneckerMap_smul_right`, `diagonal_kronecker_diagonal`, `kroneckerTMulBilinear_apply`, `kroneckerMap_transpose`, `trace_kroneckerTMul`, `mul_kroneckerTMul_mul`, `kroneckerTMul_diagonal`, `kroneckerMap_add_right`, `kroneckerMap_zero_left`, `kroneckerMap_zero_right`, `ofNat_kronecker`, `det_kroneckerTMul`, `kroneckerTMul_apply`, `kroneckerTMul_assoc`, `natCast_kronecker_natCast`, `one_kroneckerTMul_one`, `vec_mul_eq_vecMul`, `vec_mul_eq_mulVec`, `conjTranspose_kronecker'`, `kronecker_mulVec_vec_of_commute`, `kroneckerMap_add_left`, `kronecker_smul`, `kronecker_diagonal`, `IsDiag.kronecker`, `kroneckerMap_diagonal_left`, `TensorProduct.toMatrix_map`, `kronecker_zero`, `zero_kroneckerTMul`, `kroneckerLinearEquiv_tmul`
`kroneckerMapBilinear` 📖	CompOp	4 math math: `det_kroneckerMapBilinear`, `kroneckerMapBilinear_apply_apply`, `kroneckerMapBilinear_mul_mul`, `trace_kroneckerMapBilinear`
`kroneckerTMul` 📖	CompOp	—
`kroneckerTMulBilinear` 📖	CompOp	1 math math: `kroneckerTMulBilinear_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_kronecker` 📖	mathematical	—	`kroneckerMap` `Distrib.toMul` `Matrix` `add` `Distrib.toAdd`	—	`kroneckerMap_add_left` `add_mul` `Distrib.rightDistribClass`
`add_kroneckerTMul` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul` `Matrix` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `TensorProduct.add`	—	`kroneckerMap_add_left` `TensorProduct.add_tmul`
`conjTranspose_kronecker` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `CommMagma.toMul` `kroneckerMap`	—	`ext` `star_mul'`
`conjTranspose_kronecker'` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `kroneckerMap` `submatrix`	—	`ext` `StarMul.star_mul`
`conjTranspose_kroneckerTMul` 📖	mathematical	—	`conjTranspose` `TensorProduct` `TensorProduct.instStar` `kroneckerMap` `TensorProduct.tmul` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid`	—	`ext`
`det_kronecker` 📖	mathematical	—	`det` `instFintypeProd` `kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Fintype.card`	—	`smulCommClass` `smulCommClass_self` `IsScalarTower.left` `det_kroneckerMapBilinear` `mul_mul_mul_comm` `ext` `mul_one` `one_mul`
`det_kroneckerMapBilinear` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`det` `instFintypeProd` `Matrix` `addCommMonoid` `module` `smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `kroneckerMapBilinear` `Monoid.toNatPow` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `map` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Fintype.card`	—	`smulCommClass` `kroneckerMapBilinear_mul_mul` `mul_one` `one_mul` `det_mul` `diagonal_one` `kroneckerMapBilinear_apply_apply` `kroneckerMap_diagonal_right` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `kroneckerMap_diagonal_left` `LinearMap.map_zero₂` `det_reindex_self` `det_blockDiagonal` `Finset.prod_const`
`det_kroneckerTMul` 📖	mathematical	—	`det` `instFintypeProd` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instCommRing` `kroneckerMap` `TensorProduct.tmul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Fintype.card`	—	`smulCommClass` `TensorProduct.smulCommClass_left` `smulCommClass_self` `det_kroneckerMapBilinear` `Algebra.TensorProduct.tmul_mul_tmul` `Algebra.to_smulCommClass` `IsScalarTower.right` `det.congr_simp` `Algebra.TensorProduct.includeLeft_apply` `Algebra.TensorProduct.tmul_pow` `one_pow` `mul_one` `one_mul`
`diagonal_kronecker` 📖	mathematical	—	`kroneckerMap` `MulZeroClass.toMul` `diagonal` `MulZeroClass.toZero` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodComm` `blockDiagonal` `smul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toSMulWithZero`	—	`kroneckerMap_diagonal_left` `MulZeroClass.zero_mul`
`diagonal_kroneckerTMul` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul` `diagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodComm` `blockDiagonal` `TensorProduct.zero` `map`	—	`kroneckerMap_diagonal_left` `TensorProduct.zero_tmul`
`diagonal_kroneckerTMul_diagonal` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul` `diagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `TensorProduct.zero`	—	`kroneckerMap_diagonal_diagonal` `TensorProduct.zero_tmul` `TensorProduct.tmul_zero`
`diagonal_kronecker_diagonal` 📖	mathematical	—	`kroneckerMap` `MulZeroClass.toMul` `diagonal` `MulZeroClass.toZero`	—	`kroneckerMap_diagonal_diagonal` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`kroneckerMapBilinear_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `addCommMonoid` `module` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `kroneckerMapBilinear` `kroneckerMap`	—	`smulCommClass`
`kroneckerMapBilinear_mul_mul` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Matrix` `addCommMonoid` `module` `smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `kroneckerMapBilinear` `instHMulOfFintypeOfMulOfAddCommMonoid` `instFintypeProd`	—	`ext` `smulCommClass` `Finset.sum_congr` `Finset.sum_product` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.sum_apply`
`kroneckerMap_add_left` 📖	mathematical	—	`kroneckerMap` `Matrix` `add`	—	`ext`
`kroneckerMap_add_right` 📖	mathematical	—	`kroneckerMap` `Matrix` `add`	—	`ext`
`kroneckerMap_apply` 📖	mathematical	—	`kroneckerMap`	—	—
`kroneckerMap_assoc` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Matrix` `Equiv.trans` `reindex` `Equiv.prodAssoc` `Equiv.mapMatrix` `kroneckerMap`	—	`ext`
`kroneckerMap_assoc₁` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodAssoc` `kroneckerMap`	—	`ext`
`kroneckerMap_diagonal_diagonal` 📖	mathematical	—	`kroneckerMap` `diagonal`	—	`ext` `ite_apply` `ite_and`
`kroneckerMap_diagonal_left` 📖	mathematical	—	`kroneckerMap` `diagonal` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodComm` `blockDiagonal` `map`	—	`ext` `ite_apply`
`kroneckerMap_diagonal_right` 📖	mathematical	—	`kroneckerMap` `diagonal` `blockDiagonal` `map`	—	`ext`
`kroneckerMap_map` 📖	mathematical	—	`map` `kroneckerMap`	—	`ext`
`kroneckerMap_map_left` 📖	mathematical	—	`kroneckerMap` `map`	—	`ext`
`kroneckerMap_map_right` 📖	mathematical	—	`kroneckerMap` `map`	—	`ext`
`kroneckerMap_one_one` 📖	mathematical	—	`kroneckerMap` `Matrix` `one`	—	`kroneckerMap_diagonal_diagonal`
`kroneckerMap_reindex` 📖	mathematical	—	`kroneckerMap` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodCongr`	—	`ext`
`kroneckerMap_reindex_left` 📖	mathematical	—	`kroneckerMap` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodCongr` `Equiv.refl`	—	`kroneckerMap_reindex`
`kroneckerMap_reindex_right` 📖	mathematical	—	`kroneckerMap` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodCongr` `Equiv.refl`	—	`kroneckerMap_reindex`
`kroneckerMap_single_single` 📖	mathematical	—	`kroneckerMap` `single`	—	`ext`
`kroneckerMap_smul_left` 📖	mathematical	—	`kroneckerMap` `Matrix` `smul`	—	`ext`
`kroneckerMap_smul_right` 📖	mathematical	—	`kroneckerMap` `Matrix` `smul`	—	`ext`
`kroneckerMap_transpose` 📖	mathematical	—	`kroneckerMap` `transpose`	—	`ext`
`kroneckerMap_zero_left` 📖	mathematical	—	`kroneckerMap` `Matrix` `zero`	—	`ext`
`kroneckerMap_zero_right` 📖	mathematical	—	`kroneckerMap` `Matrix` `zero`	—	`ext`
`kroneckerTMulBilinear_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `TensorProduct` `addCommMonoid` `TensorProduct.addCommMonoid` `module` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.leftModule` `smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorProduct.smulCommClass_left` `kroneckerTMulBilinear` `kroneckerMap` `TensorProduct.tmul`	—	`smulCommClass` `TensorProduct.smulCommClass_left`
`kroneckerTMul_add` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul` `Matrix` `add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `TensorProduct.add`	—	`kroneckerMap_add_right` `TensorProduct.tmul_add`
`kroneckerTMul_apply` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul`	—	—
`kroneckerTMul_assoc` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodAssoc` `map` `kroneckerMap` `TensorProduct.tmul` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.assoc`	—	`ext` `RingHomInvPair.ids` `TensorProduct.assoc_tmul`
`kroneckerTMul_assoc'` 📖	mathematical	—	`submatrix` `TensorProduct` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `map` `kroneckerMap` `TensorProduct.tmul` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `TensorProduct.assoc` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `Equiv.prodAssoc`	—	`ext` `RingHomInvPair.ids` `TensorProduct.assoc_tmul`
`kroneckerTMul_diagonal` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul` `diagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `blockDiagonal` `TensorProduct.zero` `map`	—	`kroneckerMap_diagonal_right` `TensorProduct.tmul_zero`
`kroneckerTMul_smul` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `TensorProduct.leftHasSMul`	—	`kroneckerMap_smul_right` `TensorProduct.tmul_smul` `TensorProduct.CompatibleSMul.isScalarTower`
`kroneckerTMul_zero` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul` `Matrix` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `TensorProduct.zero`	—	`kroneckerMap_zero_right` `TensorProduct.tmul_zero`
`kronecker_add` 📖	mathematical	—	`kroneckerMap` `Distrib.toMul` `Matrix` `add` `Distrib.toAdd`	—	`kroneckerMap_add_right` `mul_add` `Distrib.leftDistribClass`
`kronecker_apply` 📖	mathematical	—	`kroneckerMap`	—	—
`kronecker_assoc` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodAssoc` `kroneckerMap` `Semigroup.toMul`	—	`kroneckerMap_assoc₁` `mul_assoc`
`kronecker_assoc'` 📖	mathematical	—	`submatrix` `kroneckerMap` `Semigroup.toMul` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.prodAssoc`	—	`kroneckerMap_assoc₁` `mul_assoc`
`kronecker_diagonal` 📖	mathematical	—	`kroneckerMap` `MulZeroClass.toMul` `diagonal` `MulZeroClass.toZero` `blockDiagonal` `MulOpposite` `Matrix` `smul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulOpposite.instZero` `MulZeroClass.toOppositeSMulWithZero` `MulOpposite.op`	—	`kroneckerMap_diagonal_right` `MulZeroClass.mul_zero`
`kronecker_natCast` 📖	mathematical	—	`kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `blockDiagonal` `AddMonoid.toNatSMul` `addMonoid` `AddMonoidWithOne.toAddMonoid`	—	`kronecker_diagonal` `ext` `nsmul_eq_mul` `Commute.eq` `Nat.cast_commute`
`kronecker_ofNat` 📖	mathematical	—	`kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `blockDiagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `MulOpposite` `Matrix` `smul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulOpposite.instZero` `MulZeroClass.toOppositeSMulWithZero` `MulOpposite.op`	—	`kronecker_diagonal`
`kronecker_one` 📖	mathematical	—	`kroneckerMap` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `blockDiagonal`	—	`kronecker_diagonal` `ext` `mul_one`
`kronecker_smul` 📖	mathematical	—	`kroneckerMap` `Matrix` `smul`	—	`kroneckerMap_smul_right` `mul_smul_comm`
`kronecker_zero` 📖	mathematical	—	`kroneckerMap` `MulZeroClass.toMul` `Matrix` `zero` `MulZeroClass.toZero`	—	`kroneckerMap_zero_right` `MulZeroClass.mul_zero`
`mul_kroneckerTMul_mul` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `TensorProduct.tmul` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instFintypeProd` `Algebra.TensorProduct.instMul` `TensorProduct.addCommMonoid`	—	`kroneckerMapBilinear_mul_mul` `TensorProduct.smulCommClass_left` `smulCommClass_self` `Algebra.TensorProduct.tmul_mul_tmul`
`mul_kronecker_mul` 📖	mathematical	—	`kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFintypeProd`	—	`kroneckerMapBilinear_mul_mul` `smulCommClass_self` `IsScalarTower.left` `mul_mul_mul_comm`
`natCast_kronecker` 📖	mathematical	—	`kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodComm` `blockDiagonal` `AddMonoid.toNatSMul` `addMonoid` `AddMonoidWithOne.toAddMonoid`	—	`diagonal_kronecker` `ext` `Commute.eq` `Nat.cast_commute` `nsmul_eq_mul`
`natCast_kronecker_natCast` 📖	mathematical	—	`kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Matrix` `instNatCastOfZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`diagonal_kronecker_diagonal`
`ofNat_kronecker` 📖	mathematical	—	`kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodComm` `blockDiagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul`	—	`diagonal_kronecker`
`one_kronecker` 📖	mathematical	—	`kroneckerMap` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.prodComm` `blockDiagonal`	—	`diagonal_kronecker` `ext` `one_mul`
`one_kroneckerTMul_one` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `AddCommMonoidWithOne.toAddCommMonoid` `TensorProduct.tmul` `Matrix` `one` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toOne` `TensorProduct.zero` `Algebra.TensorProduct.instOneTensorProduct`	—	`kroneckerMap_one_one` `TensorProduct.zero_tmul` `TensorProduct.tmul_zero`
`one_kronecker_one` 📖	mathematical	—	`kroneckerMap` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`kroneckerMap_one_one` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `one_mul`
`single_kroneckerTMul_single` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `TensorProduct.zero`	—	`kroneckerMap_single_single` `TensorProduct.zero_tmul` `TensorProduct.tmul_zero`
`single_kronecker_single` 📖	mathematical	—	`kroneckerMap` `MulZeroClass.toMul` `single` `MulZeroClass.toZero`	—	`kroneckerMap_single_single` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`smul_kronecker` 📖	mathematical	—	`kroneckerMap` `Matrix` `smul`	—	`kroneckerMap_smul_left` `smul_mul_assoc`
`smul_kroneckerTMul` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul` `Matrix` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `TensorProduct.leftHasSMul`	—	`kroneckerMap_smul_left` `TensorProduct.smul_tmul'`
`trace_kronecker` 📖	mathematical	—	`trace` `instFintypeProd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`trace_kroneckerMapBilinear` `smulCommClass_self` `IsScalarTower.left`
`trace_kroneckerMapBilinear` 📖	mathematical	—	`trace` `instFintypeProd` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Matrix` `addCommMonoid` `module` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `kroneckerMapBilinear`	—	`smulCommClass` `Finset.sum_congr` `LinearMap.map_sum₂` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_product`
`trace_kroneckerTMul` 📖	mathematical	—	`trace` `TensorProduct` `instFintypeProd` `TensorProduct.addCommMonoid` `kroneckerMap` `TensorProduct.tmul`	—	`trace_kroneckerMapBilinear` `TensorProduct.smulCommClass_left` `smulCommClass_self`
`zero_kronecker` 📖	mathematical	—	`kroneckerMap` `MulZeroClass.toMul` `Matrix` `zero` `MulZeroClass.toZero`	—	`kroneckerMap_zero_left` `MulZeroClass.zero_mul`
`zero_kroneckerTMul` 📖	mathematical	—	`kroneckerMap` `TensorProduct` `TensorProduct.tmul` `Matrix` `zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `TensorProduct.zero`	—	`kroneckerMap_zero_left` `TensorProduct.zero_tmul`

---

← Back to Index