Documentation Verification Report

ToTensorPower

📁 Source: Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean

Statistics

Metric	Count
Definitions `equivDirectSum`, `ofDirectSum`, `toDirectSum`, `toTensorAlgebra`	4
Theorems `equivDirectSum_apply`, `equivDirectSum_symm_apply`, `mk_reindex_cast`, `mk_reindex_fin_cast`, `ofDirectSum_comp_toDirectSum`, `ofDirectSum_of_tprod`, `ofDirectSum_toDirectSum`, `toDirectSum_comp_ofDirectSum`, `toDirectSum_ofDirectSum`, `toDirectSum_tensorPower_tprod`, `toDirectSum_ι`, `list_prod_gradedMonoid_mk_single`, `toTensorAlgebra_gMul`, `toTensorAlgebra_gOne`, `toTensorAlgebra_galgebra_toFun`, `toTensorAlgebra_tprod`	16
Total	20

TensorAlgebra

Definitions

Name	Category	Theorems
`equivDirectSum` 📖	CompOp	2 math math: `equivDirectSum_apply`, `equivDirectSum_symm_apply`
`ofDirectSum` 📖	CompOp	6 math math: `ofDirectSum_of_tprod`, `toDirectSum_ofDirectSum`, `ofDirectSum_toDirectSum`, `toDirectSum_comp_ofDirectSum`, `equivDirectSum_symm_apply`, `ofDirectSum_comp_toDirectSum`
`toDirectSum` 📖	CompOp	7 math math: `toDirectSum_tensorPower_tprod`, `toDirectSum_ofDirectSum`, `equivDirectSum_apply`, `ofDirectSum_toDirectSum`, `toDirectSum_comp_ofDirectSum`, `toDirectSum_ι`, `ofDirectSum_comp_toDirectSum`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivDirectSum_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorAlgebra` `DirectSum` `TensorPower` `PiTensorProduct.instAddCommMonoid` `instSemiringTensorAlgebra` `DirectSum.semiring` `Nat.instAddMonoid` `TensorPower.gsemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `DirectSum.instAlgebra` `PiTensorProduct.instModule` `TensorPower.galgebra` `AlgEquiv.instFunLike` `equivDirectSum` `AlgHom` `AlgHom.funLike` `toDirectSum`	—	`IsScalarTower.left`
`equivDirectSum_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `DirectSum` `TensorPower` `PiTensorProduct.instAddCommMonoid` `TensorAlgebra` `DirectSum.semiring` `Nat.instAddMonoid` `TensorPower.gsemiring` `instSemiringTensorAlgebra` `DirectSum.instAlgebra` `PiTensorProduct.instModule` `TensorPower.galgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equivDirectSum` `AlgHom` `AlgHom.funLike` `ofDirectSum`	—	`IsScalarTower.left`
`mk_reindex_cast` 📖	mathematical	—	`TensorPower` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PiTensorProduct` `PiTensorProduct.instAddCommMonoid` `PiTensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `PiTensorProduct.reindex` `Equiv.cast`	—	`RingHomInvPair.ids` `PiTensorProduct.gradedMonoid_eq_of_reindex_cast`
`mk_reindex_fin_cast` 📖	mathematical	—	`TensorPower` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PiTensorProduct` `PiTensorProduct.instAddCommMonoid` `PiTensorProduct.instModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `PiTensorProduct.reindex` `finCongr`	—	`RingHomInvPair.ids` `finCongr_eq_equivCast` `mk_reindex_cast`
`ofDirectSum_comp_toDirectSum` 📖	mathematical	—	`AlgHom.comp` `TensorAlgebra` `DirectSum` `TensorPower` `PiTensorProduct.instAddCommMonoid` `instSemiringTensorAlgebra` `DirectSum.semiring` `Nat.instAddMonoid` `TensorPower.gsemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `DirectSum.instAlgebra` `PiTensorProduct.instModule` `TensorPower.galgebra` `ofDirectSum` `toDirectSum` `AlgHom.id`	—	`hom_ext` `IsScalarTower.left` `LinearMap.ext` `RingHomCompTriple.ids` `toDirectSum_ι` `ofDirectSum_of_tprod` `mul_one`
`ofDirectSum_of_tprod` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `DirectSum` `TensorPower` `PiTensorProduct.instAddCommMonoid` `TensorAlgebra` `DirectSum.semiring` `Nat.instAddMonoid` `TensorPower.gsemiring` `instSemiringTensorAlgebra` `DirectSum.instAlgebra` `PiTensorProduct.instModule` `TensorPower.galgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `AlgHom.funLike` `ofDirectSum` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `DirectSum.of` `MultilinearMap` `PiTensorProduct` `MultilinearMap.instFunLikeForall` `PiTensorProduct.tprod` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `tprod`	—	`IsScalarTower.left` `DirectSum.toAddMonoid_of` `TensorPower.toTensorAlgebra_tprod`
`ofDirectSum_toDirectSum` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `DirectSum` `TensorPower` `PiTensorProduct.instAddCommMonoid` `TensorAlgebra` `DirectSum.semiring` `Nat.instAddMonoid` `TensorPower.gsemiring` `instSemiringTensorAlgebra` `DirectSum.instAlgebra` `PiTensorProduct.instModule` `TensorPower.galgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `AlgHom.funLike` `ofDirectSum` `toDirectSum`	—	`AlgHom.congr_fun` `IsScalarTower.left` `ofDirectSum_comp_toDirectSum`
`toDirectSum_comp_ofDirectSum` 📖	mathematical	—	`AlgHom.comp` `DirectSum` `TensorPower` `PiTensorProduct.instAddCommMonoid` `TensorAlgebra` `DirectSum.semiring` `Nat.instAddMonoid` `TensorPower.gsemiring` `instSemiringTensorAlgebra` `DirectSum.instAlgebra` `PiTensorProduct.instModule` `TensorPower.galgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `toDirectSum` `ofDirectSum` `AlgHom.id`	—	`DirectSum.algHom_ext'` `IsScalarTower.left` `PiTensorProduct.ext` `RingHomCompTriple.ids` `MultilinearMap.ext` `DirectSum.ext` `ofDirectSum_of_tprod` `toDirectSum_tensorPower_tprod`
`toDirectSum_ofDirectSum` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorAlgebra` `DirectSum` `TensorPower` `PiTensorProduct.instAddCommMonoid` `instSemiringTensorAlgebra` `DirectSum.semiring` `Nat.instAddMonoid` `TensorPower.gsemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `DirectSum.instAlgebra` `PiTensorProduct.instModule` `TensorPower.galgebra` `AlgHom.funLike` `toDirectSum` `ofDirectSum`	—	`AlgHom.congr_fun` `IsScalarTower.left` `toDirectSum_comp_ofDirectSum`
`toDirectSum_tensorPower_tprod` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorAlgebra` `DirectSum` `TensorPower` `PiTensorProduct.instAddCommMonoid` `instSemiringTensorAlgebra` `DirectSum.semiring` `Nat.instAddMonoid` `TensorPower.gsemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `DirectSum.instAlgebra` `PiTensorProduct.instModule` `TensorPower.galgebra` `AlgHom.funLike` `toDirectSum` `MultilinearMap` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `MultilinearMap.instFunLikeForall` `tprod` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `DirectSum.of` `PiTensorProduct` `PiTensorProduct.tprod`	—	`IsScalarTower.left` `tprod_apply` `map_list_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `List.map_ofFn` `toDirectSum_ι` `DirectSum.list_prod_ofFn_of_eq_dProd` `DirectSum.of_eq_of_gradedMonoid_eq` `GradedMonoid.mk_list_dProd` `TensorPower.list_prod_gradedMonoid_mk_single`
`toDirectSum_ι` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorAlgebra` `DirectSum` `TensorPower` `PiTensorProduct.instAddCommMonoid` `instSemiringTensorAlgebra` `DirectSum.semiring` `Nat.instAddMonoid` `TensorPower.gsemiring` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `DirectSum.instAlgebra` `PiTensorProduct.instModule` `TensorPower.galgebra` `AlgHom.funLike` `toDirectSum` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `ι` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `DirectSum.of` `MultilinearMap` `PiTensorProduct` `MultilinearMap.instFunLikeForall` `PiTensorProduct.tprod`	—	`IsScalarTower.left` `lift_ι_apply` `PiTensorProduct.subsingletonEquiv_symm_apply'`

TensorPower

Definitions

Name	Category	Theorems
`toTensorAlgebra` 📖	CompOp	4 math math: `toTensorAlgebra_gMul`, `toTensorAlgebra_gOne`, `toTensorAlgebra_galgebra_toFun`, `toTensorAlgebra_tprod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`list_prod_gradedMonoid_mk_single` 📖	mathematical	—	`GradedMonoid` `TensorPower` `GradedMonoid.GMul.toMul` `gMul` `GradedMonoid.GOne.toOne` `MulZeroClass.toZero` `Nat.instMulZeroClass` `gOne` `DFunLike.coe` `MultilinearMap` `PiTensorProduct` `CommSemiring.toSemiring` `PiTensorProduct.instAddCommMonoid` `PiTensorProduct.instModule` `MultilinearMap.instFunLikeForall` `PiTensorProduct.tprod`	—	`Fin.cons_zero` `Fin.cons_succ` `tprod_mul_tprod` `gradedMonoid_eq_of_cast` `add_comm` `RingHomInvPair.ids` `cast_tprod` `Fin.append_left_eq_cons`
`toTensorAlgebra_gMul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorPower` `TensorAlgebra` `PiTensorProduct.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiringTensorAlgebra` `PiTensorProduct.instModule` `Algebra.toModule` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `toTensorAlgebra` `GradedMonoid.GMul.mul` `gMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`IsScalarTower.left` `PiTensorProduct.instSMulCommClass` `TensorProduct.smulCommClass_left` `smulCommClass_self` `PiTensorProduct.instIsScalarTower` `TensorProduct.isScalarTower` `RingHomInvPair.ids` `gMul_eq_coe_linearMap` `instSMulCommClassTensorAlgebra` `instIsScalarTowerTensorAlgebra` `IsScalarTower.right` `LinearMap.compr₂_apply` `Algebra.to_smulCommClass` `LinearMap.mul_apply'` `RingHomCompTriple.ids` `LinearMap.compl₂_apply` `LinearMap.comp_apply` `LinearMap.congr_fun` `PiTensorProduct.ext` `MultilinearMap.ext` `tprod_mul_tprod` `toTensorAlgebra_tprod` `List.ofFn_comp'` `List.ofFn_fin_append` `Semigroup.to_isLawfulIdentity` `Semigroup.to_isAssociative`
`toTensorAlgebra_gOne` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorPower` `MulZeroClass.toZero` `Nat.instMulZeroClass` `TensorAlgebra` `PiTensorProduct.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiringTensorAlgebra` `PiTensorProduct.instModule` `Algebra.toModule` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `toTensorAlgebra` `GradedMonoid.GOne.one` `gOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`IsScalarTower.left` `toTensorAlgebra_tprod`
`toTensorAlgebra_galgebra_toFun` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorPower` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `TensorAlgebra` `PiTensorProduct.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiringTensorAlgebra` `PiTensorProduct.instModule` `Algebra.toModule` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `toTensorAlgebra` `AddMonoidHom` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidHom.instFunLike` `DirectSum.GAlgebra.toFun` `gsemiring` `galgebra` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.left` `RingHomInvPair.ids` `galgebra_toFun_def` `algebraMap₀_eq_smul_one` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `toTensorAlgebra_gOne` `Algebra.algebraMap_eq_smul_one`
`toTensorAlgebra_tprod` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorPower` `TensorAlgebra` `PiTensorProduct.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiringTensorAlgebra` `PiTensorProduct.instModule` `Algebra.toModule` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap.instFunLike` `toTensorAlgebra` `MultilinearMap` `PiTensorProduct` `MultilinearMap.instFunLikeForall` `PiTensorProduct.tprod` `TensorAlgebra.tprod`	—	`PiTensorProduct.lift.tprod`

---

← Back to Index