Basic

📁 Source: Mathlib/LinearAlgebra/TensorPower/Basic.lean

Statistics

Metric	Count
Definitions TensorPower, algebraMap₀, cast, gMul, gOne, galgebra, gmonoid, gsemiring, mulEquiv, «term⨂[_]^_»	10
Theorems gradedMonoid_eq_of_reindex_cast, algebraMap₀_eq_smul_one, algebraMap₀_mul, algebraMap₀_mul_algebraMap₀, algebraMap₀_one, cast_cast, cast_eq_cast, cast_refl, cast_symm, cast_tprod, cast_trans, gMul_def, gMul_eq_coe_linearMap, gOne_def, galgebra_toFun_def, gradedMonoid_eq_of_cast, mul_algebraMap₀, mul_assoc, mul_one, one_mul, tprod_mul_tprod	21
Total	31

PiTensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gradedMonoid_eq_of_reindex_cast 📖	—	PiTensorProduct DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instAddCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv reindex Equiv.cast	—	—	RingHomInvPair.ids reindex_refl

TensorPower

Definitions

Name	Category	Theorems
algebraMap₀ 📖	CompOp	6 math math: algebraMap₀_mul, algebraMap₀_one, galgebra_toFun_def, algebraMap₀_eq_smul_one, algebraMap₀_mul_algebraMap₀, mul_algebraMap₀
cast 📖	CompOp	12 math math: cast_cast, cast_trans, algebraMap₀_mul, cast_symm, mul_assoc, mul_one, algebraMap₀_mul_algebraMap₀, cast_refl, cast_tprod, cast_eq_cast, one_mul, mul_algebraMap₀
gMul 📖	CompOp	11 math math: gMul_eq_coe_linearMap, algebraMap₀_mul, mul_assoc, tprod_mul_tprod, mul_one, toTensorAlgebra_gMul, algebraMap₀_mul_algebraMap₀, gMul_def, list_prod_gradedMonoid_mk_single, one_mul, mul_algebraMap₀
gOne 📖	CompOp	7 math math: algebraMap₀_one, algebraMap₀_eq_smul_one, mul_one, toTensorAlgebra_gOne, list_prod_gradedMonoid_mk_single, gOne_def, one_mul
galgebra 📖	CompOp	11 math math: TensorAlgebra.ofDirectSum_of_tprod, TensorAlgebra.toDirectSum_tensorPower_tprod, TensorAlgebra.toDirectSum_ofDirectSum, TensorAlgebra.equivDirectSum_apply, galgebra_toFun_def, TensorAlgebra.ofDirectSum_toDirectSum, TensorAlgebra.toDirectSum_comp_ofDirectSum, TensorAlgebra.equivDirectSum_symm_apply, toTensorAlgebra_galgebra_toFun, TensorAlgebra.toDirectSum_ι, TensorAlgebra.ofDirectSum_comp_toDirectSum
gmonoid 📖	CompOp	—
gsemiring 📖	CompOp	11 math math: TensorAlgebra.ofDirectSum_of_tprod, TensorAlgebra.toDirectSum_tensorPower_tprod, TensorAlgebra.toDirectSum_ofDirectSum, TensorAlgebra.equivDirectSum_apply, galgebra_toFun_def, TensorAlgebra.ofDirectSum_toDirectSum, TensorAlgebra.toDirectSum_comp_ofDirectSum, TensorAlgebra.equivDirectSum_symm_apply, toTensorAlgebra_galgebra_toFun, TensorAlgebra.toDirectSum_ι, TensorAlgebra.ofDirectSum_comp_toDirectSum
mulEquiv 📖	CompOp	2 math math: gMul_eq_coe_linearMap, gMul_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap₀_eq_smul_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PiTensorProduct.instAddCommMonoid Semiring.toModule PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv algebraMap₀ MulZeroClass.toZero Nat.instMulZeroClass PiTensorProduct.instSMul GradedMonoid.GOne.one gOne	—	RingHomInvPair.ids Fin.isEmpty'
algebraMap₀_mul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Nat.instAddMonoid AddZero.toZero PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cast zero_add GradedMonoid.GMul.mul gMul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule algebraMap₀ PiTensorProduct.instSMul	—	RingHomInvPair.ids zero_add PiTensorProduct.instSMulCommClass TensorProduct.smulCommClass_left smulCommClass_self PiTensorProduct.instIsScalarTower TensorProduct.isScalarTower gMul_eq_coe_linearMap algebraMap₀_eq_smul_one LinearMap.map_smul₂ map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass one_mul
algebraMap₀_mul_algebraMap₀ 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Nat.instAddMonoid AddZero.toZero PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cast add_zero GradedMonoid.GMul.mul gMul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule algebraMap₀ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	RingHomInvPair.ids add_zero smul_eq_mul map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass algebraMap₀_mul
algebraMap₀_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PiTensorProduct.instAddCommMonoid Semiring.toModule PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv algebraMap₀ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne GradedMonoid.GOne.one MulZeroClass.toZero Nat.instMulZeroClass gOne	—	RingHomInvPair.ids algebraMap₀_eq_smul_one one_smul Algebra.to_smulCommClass
cast_cast 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cast	—	PiTensorProduct.reindex_reindex
cast_eq_cast 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cast	—	RingHomInvPair.ids cast_refl
cast_refl 📖	mathematical	—	cast LinearEquiv.refl TensorPower CommSemiring.toSemiring PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule	—	RingHomInvPair.ids finCongr_refl PiTensorProduct.reindex_refl
cast_symm 📖	mathematical	—	LinearEquiv.symm TensorPower CommSemiring.toSemiring PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids cast	—	PiTensorProduct.reindex_symm
cast_tprod 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cast MultilinearMap PiTensorProduct MultilinearMap.instFunLikeForall PiTensorProduct.tprod	—	PiTensorProduct.reindex_tprod
cast_trans 📖	mathematical	—	LinearEquiv.trans TensorPower CommSemiring.toSemiring PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids RingHomInvPair.ids cast	—	PiTensorProduct.reindex_trans
gMul_def 📖	mathematical	—	GradedMonoid.GMul.mul TensorPower gMul DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv mulEquiv TensorProduct.tmul	—	—
gMul_eq_coe_linearMap 📖	mathematical	—	GradedMonoid.GMul.mul TensorPower gMul DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module PiTensorProduct.instSMulCommClass LinearMap.compr₂ TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Semiring.toModule PiTensorProduct.instIsScalarTower TensorProduct.isScalarTower SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearEquiv.toLinearMap RingHomInvPair.ids mulEquiv	—	—
gOne_def 📖	mathematical	—	GradedMonoid.GOne.one TensorPower MulZeroClass.toZero Nat.instMulZeroClass gOne DFunLike.coe MultilinearMap PiTensorProduct CommSemiring.toSemiring PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule MultilinearMap.instFunLikeForall PiTensorProduct.tprod	—	—
galgebra_toFun_def 📖	mathematical	—	DFunLike.coe AddMonoidHom TensorPower AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Nat.instAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommMonoid.toAddMonoid PiTensorProduct.instAddCommMonoid AddMonoidHom.instFunLike DirectSum.GAlgebra.toFun PiTensorProduct.instModule gsemiring galgebra LinearEquiv RingHom.id RingHomInvPair.ids NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv algebraMap₀	—	—
gradedMonoid_eq_of_cast 📖	—	PiTensorProduct DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cast	—	—	RingHomInvPair.ids PiTensorProduct.gradedMonoid_eq_of_reindex_cast finCongr_eq_equivCast cast.eq_1
mul_algebraMap₀ 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Nat.instAddMonoid AddZero.toZero PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cast add_zero GradedMonoid.GMul.mul gMul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule algebraMap₀ PiTensorProduct.instSMul	—	RingHomInvPair.ids add_zero PiTensorProduct.instSMulCommClass TensorProduct.smulCommClass_left smulCommClass_self PiTensorProduct.instIsScalarTower TensorProduct.isScalarTower gMul_eq_coe_linearMap algebraMap₀_eq_smul_one map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass mul_one
mul_assoc 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower AddSemigroup.toAdd Nat.instAddSemigroup PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cast add_assoc GradedMonoid.GMul.mul gMul	—	PiTensorProduct.instSMulCommClass TensorProduct.smulCommClass_left smulCommClass_self PiTensorProduct.instIsScalarTower TensorProduct.isScalarTower RingHomInvPair.ids add_assoc LinearMap.instSMulCommClass RingHomCompTriple.ids SMulCommClass.symm PiTensorProduct.ext MultilinearMap.ext tprod_mul_tprod cast_tprod Fin.append_assoc LinearMap.congr_fun
mul_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Nat.instAddMonoid AddZero.toZero PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cast add_zero GradedMonoid.GMul.mul gMul GradedMonoid.GOne.one MulZeroClass.toZero Nat.instMulZeroClass gOne	—	RingHomInvPair.ids add_zero gMul_def gOne_def PiTensorProduct.induction_on Algebra.to_smulCommClass PiTensorProduct.instSMulCommClass TensorProduct.smul_tmul' map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass tprod_mul_tprod cast_tprod Fin.append_elim0 TensorProduct.add_tmul map_add SemilinearMapClass.toAddHomClass
one_mul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorPower AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass Nat.instAddMonoid AddZero.toZero PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv cast zero_add GradedMonoid.GMul.mul gMul GradedMonoid.GOne.one MulZeroClass.toZero Nat.instMulZeroClass gOne	—	RingHomInvPair.ids zero_add gMul_def gOne_def PiTensorProduct.induction_on Algebra.to_smulCommClass PiTensorProduct.instSMulCommClass TensorProduct.tmul_smul TensorProduct.CompatibleSMul.isScalarTower PiTensorProduct.instIsScalarTower map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass tprod_mul_tprod cast_tprod Fin.elim0_append TensorProduct.tmul_add map_add SemilinearMapClass.toAddHomClass
tprod_mul_tprod 📖	mathematical	—	GradedMonoid.GMul.mul TensorPower gMul DFunLike.coe MultilinearMap PiTensorProduct CommSemiring.toSemiring PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule MultilinearMap.instFunLikeForall PiTensorProduct.tprod Fin.append	—	RingHomInvPair.ids PiTensorProduct.tmulEquiv_apply PiTensorProduct.reindex_tprod

TensorProduct

Definitions

Name	Category	Theorems
«term⨂[_]^_» 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
TensorPower 📖	CompOp	38 math math: TensorAlgebra.ofDirectSum_of_tprod, TensorPower.cast_cast, TensorPower.cast_trans, TensorAlgebra.toDirectSum_tensorPower_tprod, TensorPower.gMul_eq_coe_linearMap, TensorPower.algebraMap₀_mul, TensorAlgebra.toDirectSum_ofDirectSum, TensorPower.cast_symm, TensorPower.mul_assoc, TensorPower.algebraMap₀_one, TensorAlgebra.equivDirectSum_apply, TensorPower.galgebra_toFun_def, TensorPower.tprod_mul_tprod, TensorPower.algebraMap₀_eq_smul_one, TensorPower.multilinearMapToDual_apply_tprod, TensorAlgebra.ofDirectSum_toDirectSum, TensorPower.mul_one, TensorPower.toTensorAlgebra_gMul, TensorPower.toTensorAlgebra_gOne, TensorAlgebra.toDirectSum_comp_ofDirectSum, TensorPower.algebraMap₀_mul_algebraMap₀, TensorPower.gMul_def, TensorPower.list_prod_gradedMonoid_mk_single, TensorPower.cast_refl, TensorPower.cast_tprod, TensorPower.cast_eq_cast, TensorPower.gOne_def, TensorPower.one_mul, TensorAlgebra.equivDirectSum_symm_apply, TensorAlgebra.mk_reindex_fin_cast, TensorPower.mul_algebraMap₀, TensorAlgebra.mk_reindex_cast, TensorPower.toTensorAlgebra_galgebra_toFun, TensorAlgebra.toDirectSum_ι, TensorAlgebra.ofDirectSum_comp_toDirectSum, exteriorPower.toTensorPower_apply_ιMulti, TensorPower.toTensorAlgebra_tprod, TensorPower.pairingDual_tprod_tprod

---

← Back to Index