Internal

📁 Source: Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

Statistics

Metric	Count
Definitions GradedTensorProduct, auxEquiv, comm, includeLeft, includeLeftRingHom, includeRight, instAddCommGroupWithOne, instAlgebra, instModule, instMonoid, instMul, instRing, liftEquiv, mulHom, of, tmul, «term_ᵍ⊗ₜ[_]_», «term_ᵍ⊗ₜ_», «term_ᵍ⊗[_]_»	19
Theorems algHom_ext, algHom_ext_iff, algebraMap_def, algebraMap_def', auxEquiv_comm, auxEquiv_mul, auxEquiv_one, auxEquiv_symm_one, auxEquiv_tmul, comm_coe_tmul_coe, hom_ext, hom_ext_iff, includeLeftRingHom_apply, includeLeft_apply, includeRight_apply, lift_tmul, mulHom_apply, mul_def, of_one, of_symm_of, of_symm_one, symm_of_of, tmul_algebraMap_mul_coe_tmul, tmul_coe_mul_algebraMap_tmul, tmul_coe_mul_coe_tmul, tmul_coe_mul_one_tmul, tmul_coe_mul_zero_coe_tmul, tmul_one_mul_coe_tmul, tmul_one_mul_one_tmul, tmul_zero_coe_mul_coe_tmul	30
Total	49

GradedTensorProduct

Definitions

Name	Category	Theorems
auxEquiv 📖	CompOp	6 math math: auxEquiv_one, auxEquiv_symm_one, auxEquiv_comm, auxEquiv_mul, mulHom_apply, auxEquiv_tmul
comm 📖	CompOp	2 math math: auxEquiv_comm, comm_coe_tmul_coe
includeLeft 📖	CompOp	2 math math: includeLeft_apply, algHom_ext_iff
includeLeftRingHom 📖	CompOp	1 math math: includeLeftRingHom_apply
includeRight 📖	CompOp	2 math math: algHom_ext_iff, includeRight_apply
instAddCommGroupWithOne 📖	CompOp	12 math math: hom_ext_iff, auxEquiv_one, mul_def, auxEquiv_symm_one, auxEquiv_comm, auxEquiv_mul, mulHom_apply, auxEquiv_tmul, of_symm_of, of_one, symm_of_of, of_symm_one
instAlgebra 📖	CompOp	15 math math: lift_tmul, CliffordAlgebra.toProd_comp_ofProd, CliffordAlgebra.toProd_ι_tmul_one, includeLeft_apply, auxEquiv_comm, algHom_ext_iff, includeRight_apply, algebraMap_def', CliffordAlgebra.prodEquiv_symm_apply, CliffordAlgebra.prodEquiv_apply, algebraMap_def, CliffordAlgebra.ofProd_comp_toProd, comm_coe_tmul_coe, CliffordAlgebra.toProd_one_tmul_ι, CliffordAlgebra.ofProd_ι_mk
instModule 📖	CompOp	12 math math: hom_ext_iff, auxEquiv_one, mul_def, auxEquiv_symm_one, auxEquiv_comm, auxEquiv_mul, mulHom_apply, auxEquiv_tmul, of_symm_of, of_one, symm_of_of, of_symm_one
instMonoid 📖	CompOp	—
instMul 📖	CompOp	10 math math: tmul_zero_coe_mul_coe_tmul, tmul_coe_mul_one_tmul, tmul_coe_mul_coe_tmul, mul_def, tmul_one_mul_one_tmul, tmul_one_mul_coe_tmul, auxEquiv_mul, tmul_coe_mul_zero_coe_tmul, tmul_algebraMap_mul_coe_tmul, tmul_coe_mul_algebraMap_tmul
instRing 📖	CompOp	17 math math: lift_tmul, CliffordAlgebra.toProd_comp_ofProd, CliffordAlgebra.toProd_ι_tmul_one, tmul_coe_mul_coe_tmul, includeLeft_apply, auxEquiv_comm, algHom_ext_iff, includeRight_apply, algebraMap_def', CliffordAlgebra.prodEquiv_symm_apply, includeLeftRingHom_apply, CliffordAlgebra.prodEquiv_apply, algebraMap_def, CliffordAlgebra.ofProd_comp_toProd, comm_coe_tmul_coe, CliffordAlgebra.toProd_one_tmul_ι, CliffordAlgebra.ofProd_ι_mk
liftEquiv 📖	CompOp	—
mulHom 📖	CompOp	2 math math: mul_def, mulHom_apply
of 📖	CompOp	5 math math: hom_ext_iff, of_symm_of, of_one, symm_of_of, of_symm_one
tmul 📖	CompOp	19 math math: tmul_zero_coe_mul_coe_tmul, lift_tmul, CliffordAlgebra.toProd_ι_tmul_one, tmul_coe_mul_one_tmul, tmul_coe_mul_coe_tmul, tmul_one_mul_one_tmul, includeLeft_apply, tmul_one_mul_coe_tmul, includeRight_apply, algebraMap_def', auxEquiv_tmul, includeLeftRingHom_apply, algebraMap_def, tmul_coe_mul_zero_coe_tmul, comm_coe_tmul_coe, CliffordAlgebra.toProd_one_tmul_ι, tmul_algebraMap_mul_coe_tmul, CliffordAlgebra.ofProd_ι_mk, tmul_coe_mul_algebraMap_tmul
«term_ᵍ⊗ₜ[_]_» 📖	CompOp	—
«term_ᵍ⊗ₜ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algHom_ext 📖	—	AlgHom.comp GradedTensorProduct CommRing.toCommSemiring Ring.toSemiring instRing instAlgebra includeLeft includeRight	—	—	Equiv.injective
algHom_ext_iff 📖	mathematical	—	AlgHom.comp GradedTensorProduct CommRing.toCommSemiring Ring.toSemiring instRing instAlgebra includeLeft includeRight	—	algHom_ext
algebraMap_def 📖	mathematical	—	DFunLike.coe RingHom GradedTensorProduct Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring instRing RingHom.instFunLike algebraMap instAlgebra tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
algebraMap_def' 📖	mathematical	—	DFunLike.coe RingHom GradedTensorProduct Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring instRing RingHom.instFunLike algebraMap instAlgebra tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	AlgHom.commutes
auxEquiv_comm 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids GradedTensorProduct TensorProduct DirectSum Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.addCommMonoid instModule TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv auxEquiv AlgEquiv instRing instAlgebra AlgEquiv.instFunLike comm AddCommGroup.toAddCommMonoid Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup TensorProduct.gradedComm	—	RingHomInvPair.ids LinearEquiv.eq_symm_apply
auxEquiv_mul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids GradedTensorProduct TensorProduct DirectSum Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.addCommMonoid instModule TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv auxEquiv instMul LinearMap AddCommGroup.toAddCommMonoid Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup TensorProduct.leftModule DirectSum.instSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module TensorProduct.smulCommClass_left TensorProduct.gradedMul SetLike.gring AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Submodule.addSubgroupClass GradedRing.toGradedMonoid Submodule.galgebra	—	RingHomInvPair.ids DirectSum.instSMulCommClass smulCommClass_self TensorProduct.smulCommClass_left Submodule.addSubgroupClass GradedRing.toGradedMonoid LinearEquiv.eq_symm_apply
auxEquiv_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids GradedTensorProduct TensorProduct DirectSum Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.addCommMonoid instModule TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv auxEquiv AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne Algebra.TensorProduct.instOneTensorProduct NonAssocSemiring.toAddCommMonoidWithOne DirectSum.semiring AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne SetLike.gsemiring Submodule.addSubmonoidClass GradedRing.toGradedMonoid	—	RingHomInvPair.ids Submodule.addSubmonoidClass GradedRing.toGradedMonoid of_one Algebra.TensorProduct.one_def auxEquiv_tmul SetLike.GradedMonoid.toGradedOne DirectSum.decompose_one
auxEquiv_symm_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct DirectSum Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module GradedTensorProduct TensorProduct.addCommMonoid AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.instModule instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm auxEquiv Algebra.TensorProduct.instOneTensorProduct NonAssocSemiring.toAddCommMonoidWithOne DirectSum.semiring AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne SetLike.gsemiring Submodule.addSubmonoidClass GradedRing.toGradedMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne	—	RingHomInvPair.ids Submodule.addSubmonoidClass GradedRing.toGradedMonoid LinearEquiv.symm_apply_eq auxEquiv_one
auxEquiv_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids GradedTensorProduct TensorProduct DirectSum Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.addCommMonoid instModule TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv auxEquiv tmul TensorProduct.tmul AddSubmonoidClass.toAddCommMonoid Submodule.addSubmonoidClass Equiv Equiv.instEquivLike DirectSum.decompose GradedRing.toDecomposition AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids
comm_coe_tmul_coe 📖	mathematical	—	DFunLike.coe AlgEquiv GradedTensorProduct CommRing.toCommSemiring Ring.toSemiring instRing instAlgebra AlgEquiv.instFunLike comm tmul Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule SetLike.instMembership Submodule.setLike Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Int.instUnitsPow Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	LinearEquiv.injective RingHomInvPair.ids auxEquiv_comm Submodule.addSubmonoidClass DirectSum.decompose_coe TensorProduct.gradedComm_of_tmul_of Units.smul_def Submodule.addSubgroupClass Int.cast_smul_eq_zsmul LinearEquiv.map_smul auxEquiv_tmul
hom_ext 📖	—	LinearMap.comp TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring GradedTensorProduct CommSemiring.toSemiring TensorProduct.addCommMonoid AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.instModule instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids of	—	—	RingHomCompTriple.ids RingHomInvPair.ids
hom_ext_iff 📖	mathematical	—	LinearMap.comp TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring GradedTensorProduct CommSemiring.toSemiring TensorProduct.addCommMonoid AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.instModule instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids of	—	RingHomCompTriple.ids RingHomInvPair.ids hom_ext
includeLeftRingHom_apply 📖	mathematical	—	DFunLike.coe RingHom GradedTensorProduct Semiring.toNonAssocSemiring Ring.toSemiring instRing RingHom.instFunLike includeLeftRingHom tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
includeLeft_apply 📖	mathematical	—	DFunLike.coe AlgHom GradedTensorProduct CommRing.toCommSemiring Ring.toSemiring instRing instAlgebra AlgHom.funLike includeLeft tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
includeRight_apply 📖	mathematical	—	DFunLike.coe AlgHom GradedTensorProduct CommRing.toCommSemiring Ring.toSemiring instRing instAlgebra AlgHom.funLike includeRight tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
lift_tmul 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule SetLike.instMembership Submodule.setLike Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Int.instUnitsPow Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	GradedTensorProduct instRing instAlgebra lift tmul	—	—
mulHom_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring GradedTensorProduct AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing mulHom LinearEquiv RingHomInvPair.ids TensorProduct DirectSum Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid instAddCommMonoidDirectSum DirectSum.instModule Submodule.module TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm auxEquiv AddCommGroup.toAddCommMonoid Submodule.addCommGroup Ring.toAddCommGroup TensorProduct.leftModule DirectSum.instSMulCommClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup TensorProduct.smulCommClass_left TensorProduct.gradedMul SetLike.gring AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Submodule.addSubgroupClass GradedRing.toGradedMonoid Submodule.galgebra	—	smulCommClass_self
mul_def 📖	mathematical	—	GradedTensorProduct instMul DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne instModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing mulHom	—	—
of_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring GradedTensorProduct TensorProduct.addCommMonoid AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.instModule instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv of Algebra.TensorProduct.instOneTensorProduct NonAssocSemiring.toAddCommMonoidWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne	—	RingHomInvPair.ids
of_symm_of 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids GradedTensorProduct TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.addCommMonoid instModule TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm of	—	RingHomInvPair.ids
of_symm_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids GradedTensorProduct TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.addCommMonoid instModule TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm of AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne Algebra.TensorProduct.instOneTensorProduct NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids
symm_of_of 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring GradedTensorProduct TensorProduct.addCommMonoid AddCommMonoidWithOne.toAddCommMonoid AddCommGroupWithOne.toAddCommMonoidWithOne instAddCommGroupWithOne TensorProduct.instModule instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv of LinearEquiv.symm	—	RingHomInvPair.ids
tmul_algebraMap_mul_coe_tmul 📖	mathematical	—	GradedTensorProduct instMul tmul DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring RingHom.instFunLike algebraMap Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule SetLike.instMembership Submodule.setLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	tmul_zero_coe_mul_coe_tmul Submodule.addSubmonoidClass GradedRing.toGradedMonoid
tmul_coe_mul_algebraMap_tmul 📖	mathematical	—	GradedTensorProduct instMul tmul Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	tmul_coe_mul_zero_coe_tmul Submodule.addSubmonoidClass GradedRing.toGradedMonoid
tmul_coe_mul_coe_tmul 📖	mathematical	—	GradedTensorProduct instMul tmul Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instRing Int.instUnitsPow Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	RingHomInvPair.ids DirectSum.instSMulCommClass smulCommClass_self TensorProduct.smulCommClass_left Submodule.addSubgroupClass GradedRing.toGradedMonoid Submodule.addSubmonoidClass DirectSum.decompose_coe TensorProduct.tmul_of_gradedMul_of_tmul Units.smul_def Int.cast_smul_eq_zsmul LinearEquiv.map_smul map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass TensorProduct.congr_symm_tmul DirectSum.decompose_symm_mul DirectSum.decompose_symm_of Equiv.symm_apply_apply
tmul_coe_mul_one_tmul 📖	mathematical	—	GradedTensorProduct instMul tmul Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	SetLike.GradedMonoid.toGradedOne GradedRing.toGradedMonoid SetLike.coe_gOne mul_one tmul_coe_mul_zero_coe_tmul
tmul_coe_mul_zero_coe_tmul 📖	mathematical	—	GradedTensorProduct instMul tmul Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	tmul_coe_mul_coe_tmul MulZeroClass.mul_zero uzpow_zero one_smul
tmul_one_mul_coe_tmul 📖	mathematical	—	GradedTensorProduct instMul tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	SetLike.GradedMonoid.toGradedOne GradedRing.toGradedMonoid SetLike.coe_gOne one_mul tmul_zero_coe_mul_coe_tmul
tmul_one_mul_one_tmul 📖	mathematical	—	GradedTensorProduct instMul tmul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	SetLike.GradedMonoid.toGradedOne GradedRing.toGradedMonoid SetLike.coe_gOne mul_one one_mul tmul_coe_mul_zero_coe_tmul
tmul_zero_coe_mul_coe_tmul 📖	mathematical	—	GradedTensorProduct instMul tmul Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership Submodule.setLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	tmul_coe_mul_coe_tmul MulZeroClass.zero_mul uzpow_zero one_smul

TensorProduct

Definitions

Name	Category	Theorems
«term_ᵍ⊗[_]_» 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
GradedTensorProduct 📖	CompOp	35 math math: GradedTensorProduct.hom_ext_iff, GradedTensorProduct.tmul_zero_coe_mul_coe_tmul, GradedTensorProduct.lift_tmul, CliffordAlgebra.toProd_comp_ofProd, CliffordAlgebra.toProd_ι_tmul_one, GradedTensorProduct.auxEquiv_one, GradedTensorProduct.tmul_coe_mul_one_tmul, GradedTensorProduct.tmul_coe_mul_coe_tmul, GradedTensorProduct.mul_def, GradedTensorProduct.tmul_one_mul_one_tmul, GradedTensorProduct.includeLeft_apply, GradedTensorProduct.auxEquiv_symm_one, GradedTensorProduct.auxEquiv_comm, GradedTensorProduct.tmul_one_mul_coe_tmul, GradedTensorProduct.auxEquiv_mul, GradedTensorProduct.algHom_ext_iff, GradedTensorProduct.includeRight_apply, GradedTensorProduct.mulHom_apply, GradedTensorProduct.algebraMap_def', GradedTensorProduct.auxEquiv_tmul, CliffordAlgebra.prodEquiv_symm_apply, GradedTensorProduct.includeLeftRingHom_apply, CliffordAlgebra.prodEquiv_apply, GradedTensorProduct.algebraMap_def, CliffordAlgebra.ofProd_comp_toProd, GradedTensorProduct.tmul_coe_mul_zero_coe_tmul, GradedTensorProduct.comm_coe_tmul_coe, CliffordAlgebra.toProd_one_tmul_ι, GradedTensorProduct.of_symm_of, GradedTensorProduct.tmul_algebraMap_mul_coe_tmul, CliffordAlgebra.ofProd_ι_mk, GradedTensorProduct.tmul_coe_mul_algebraMap_tmul, GradedTensorProduct.of_one, GradedTensorProduct.symm_of_of, GradedTensorProduct.of_symm_one

---

← Back to Index