Basic

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

Statistics

Metric	Count
Definitions toTensor, TensorAlgebra, algebraMapInv, instRing, toTrivSqZeroExt, tprod, ι, ιInv, instAlgebra, instInhabitedTensorAlgebra, instSemiringTensorAlgebra	11
Theorems toTensor_ι, adjoin_range_ι, algebraMap_eq_one_iff, algebraMap_eq_zero_iff, algebraMap_inj, algebraMap_leftInverse, hom_ext, hom_ext_iff, induction, instNontrivial, lift_comp_ι, lift_symm_apply, lift_unique, lift_ι_apply, range_lift, ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι, toTrivSqZeroExt_ι, tprod_apply, ι_comp_lift, ι_def, ι_eq_algebraMap_iff, ι_eq_zero_iff, ι_inj, ι_leftInverse, ι_ne_one, ι_range_disjoint_one, instIsScalarTowerTensorAlgebra, instSMulCommClassTensorAlgebra	28
Total	39

FreeAlgebra

Definitions

Name	Category	Theorems
toTensor 📖	CompOp	1 math math: toTensor_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toTensor_ι 📖	mathematical	—	DFunLike.coe AlgHom FreeAlgebra TensorAlgebra instSemiring instSemiringTensorAlgebra instAlgebra Algebra.id instAlgebra IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AlgHom.funLike toTensor ι LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike TensorAlgebra.ι	—	IsScalarTower.left lift_ι_apply

TensorAlgebra

Definitions

Name	Category	Theorems
algebraMapInv 📖	CompOp	1 math math: algebraMap_leftInverse
instRing 📖	CompOp	1 math math: rank_eq
toTrivSqZeroExt 📖	CompOp	1 math math: toTrivSqZeroExt_ι
tprod 📖	CompOp	4 math math: ofDirectSum_of_tprod, toDirectSum_tensorPower_tprod, tprod_apply, TensorPower.toTensorAlgebra_tprod
ι 📖	CompOp	27 math math: toTrivSqZeroExt_ι, ι_comp_lift, adjoin_range_ι, ι_def, toExterior_ι, equivFreeAlgebra_symm_ι, LinearAlgebra.FreeProduct.ι_apply, lift_symm_apply, equivFreeAlgebra_ι_apply, lift_ι_apply, toClifford_ι, lift_comp_ι, ι_range_disjoint_one, FreeAlgebra.toTensor_ι, ι_leftInverse, UniversalEnvelopingAlgebra.ι_apply, GradedAlgebra.ι_apply, hom_ext_iff, LinearAlgebra.FreeProduct.rel_id, tprod_apply, ι_inj, ι_eq_zero_iff, toDirectSum_ι, lift_unique, ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι, ι_eq_algebraMap_iff, UniversalEnvelopingAlgebra.lift_ι_apply'
ιInv 📖	CompOp	1 math math: ι_leftInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_range_ι 📖	mathematical	—	Algebra.adjoin TensorAlgebra instSemiringTensorAlgebra instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Set.range DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike ι Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique IsScalarTower.left induction algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass Subalgebra.instSMulMemClass Algebra.subset_adjoin Set.mem_range_self MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass
algebraMap_eq_one_iff 📖	mathematical	—	DFunLike.coe RingHom TensorAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring instSemiringTensorAlgebra RingHom.instFunLike algebraMap instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	map_eq_one_iff MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsScalarTower.left algebraMap_leftInverse
algebraMap_eq_zero_iff 📖	mathematical	—	DFunLike.coe RingHom TensorAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring instSemiringTensorAlgebra RingHom.instFunLike algebraMap instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsScalarTower.left algebraMap_leftInverse
algebraMap_inj 📖	mathematical	—	DFunLike.coe RingHom TensorAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring instSemiringTensorAlgebra RingHom.instFunLike algebraMap instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left algebraMap_leftInverse
algebraMap_leftInverse 📖	mathematical	—	TensorAlgebra DFunLike.coe AlgHom instSemiringTensorAlgebra CommSemiring.toSemiring instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AlgHom.funLike algebraMapInv RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	IsScalarTower.left AlgHom.commutes
hom_ext 📖	—	LinearMap.comp TensorAlgebra CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap ι	—	—	IsScalarTower.left RingHomCompTriple.ids Equiv.injective lift_symm_apply
hom_ext_iff 📖	mathematical	—	LinearMap.comp TensorAlgebra CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap ι	—	IsScalarTower.left RingHomCompTriple.ids hom_ext
induction 📖	—	DFunLike.coe RingHom TensorAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring instSemiringTensorAlgebra RingHom.instFunLike algebraMap instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike ι Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd	—	—	IsScalarTower.left RingHom.map_one RingHom.map_zero hom_ext LinearMap.ext RingHomCompTriple.ids lift_ι_apply AlgHom.id_apply Subtype.prop
instNontrivial 📖	mathematical	—	Nontrivial TensorAlgebra	—	Function.Injective.nontrivial IsScalarTower.left algebraMap_leftInverse
lift_comp_ι 📖	mathematical	—	DFunLike.coe Equiv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule AlgHom TensorAlgebra instSemiringTensorAlgebra instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike Equiv.instEquivLike lift LinearMap.comp RingHomCompTriple.ids AlgHom.toLinearMap ι	—	IsScalarTower.left RingHomCompTriple.ids lift_symm_apply Equiv.apply_symm_apply
lift_symm_apply 📖	mathematical	—	DFunLike.coe Equiv AlgHom TensorAlgebra instSemiringTensorAlgebra instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift LinearMap.comp AlgHom.toLinearMap ι	—	IsScalarTower.left
lift_unique 📖	mathematical	—	LinearMap.comp TensorAlgebra CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap ι DFunLike.coe Equiv LinearMap AlgHom EquivLike.toFunLike Equiv.instEquivLike lift	—	IsScalarTower.left RingHomCompTriple.ids Equiv.symm_apply_eq
lift_ι_apply 📖	mathematical	—	DFunLike.coe AlgHom TensorAlgebra instSemiringTensorAlgebra instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AlgHom.funLike Equiv LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule EquivLike.toFunLike Equiv.instEquivLike lift LinearMap.instFunLike ι	—	IsScalarTower.left RingHomCompTriple.ids ι_comp_lift
range_lift 📖	mathematical	—	AlgHom.range TensorAlgebra instSemiringTensorAlgebra instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction DFunLike.coe Equiv LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule AlgHom EquivLike.toFunLike Equiv.instEquivLike lift Algebra.adjoin Set.range LinearMap.instFunLike	—	IsScalarTower.left AlgHom.map_adjoin lift_ι_apply
ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι 📖	mathematical	—	DFunLike.coe AlgHom FreeAlgebra RingQuot FreeAlgebra.instSemiring Rel RingQuot.instSemiring FreeAlgebra.instAlgebra Algebra.id RingQuot.instAlgebra AlgHom.funLike RingQuot.mkAlgHom FreeAlgebra.ι LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike ι	—	IsScalarTower.left ι_def
toTrivSqZeroExt_ι 📖	mathematical	—	DFunLike.coe AlgHom TensorAlgebra TrivSqZeroExt instSemiringTensorAlgebra TrivSqZeroExt.semiring CommSemiring.toSemiring IsScalarTower.to_smulCommClass MulOpposite MulOpposite.instSemiring MulOpposite.instAlgebra Algebra.id IsScalarTower.op_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul IsScalarTower.left DistribMulAction.toMulAction instAlgebra TrivSqZeroExt.instAlgebra AlgHom.funLike toTrivSqZeroExt LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike ι TrivSqZeroExt.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	lift_ι_apply
tprod_apply 📖	mathematical	—	DFunLike.coe MultilinearMap TensorAlgebra CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction MultilinearMap.instFunLikeForall tprod Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne LinearMap RingHom.id LinearMap.instFunLike ι	—	IsScalarTower.left
ι_comp_lift 📖	mathematical	—	LinearMap.comp TensorAlgebra CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap DFunLike.coe Equiv LinearMap AlgHom EquivLike.toFunLike Equiv.instEquivLike lift ι	—	IsScalarTower.left RingHomCompTriple.ids Equiv.symm_apply_apply
ι_def 📖	mathematical	—	ι CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe AlgHom FreeAlgebra RingQuot FreeAlgebra.instSemiring Rel RingQuot.instSemiring FreeAlgebra.instAlgebra RingQuot.instAlgebra AlgHom.funLike RingQuot.mkAlgHom FreeAlgebra.ι	—	IsScalarTower.left
ι_eq_algebraMap_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike ι RingHom RingHom.instFunLike algebraMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	IsScalarTower.left mul_comm IsScalarTower.to_smulCommClass IsScalarTower.op_right lift_ι_apply AlgHom.commutes map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
ι_eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike ι MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	IsScalarTower.left map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
ι_inj 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike ι	—	IsScalarTower.left ι_leftInverse
ι_leftInverse 📖	mathematical	—	TensorAlgebra DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike ιInv ι	—	IsScalarTower.left toTrivSqZeroExt_ι
ι_ne_one 📖	—	—	—	—	IsScalarTower.left RingHom.map_one ι_eq_algebraMap_iff one_ne_zero NeZero.one
ι_range_disjoint_one 📖	mathematical	—	Disjoint Submodule TensorAlgebra CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringTensorAlgebra Algebra.toModule instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPartialOrder Submodule.instOrderBot LinearMap.range RingHom.id RingHomSurjective.ids ι Submodule.one	—	IsScalarTower.left RingHomSurjective.ids Submodule.disjoint_def Submodule.one_eq_range ι_eq_algebraMap_iff Algebra.linearMap_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass

(root)

Definitions

Name	Category	Theorems
TensorAlgebra 📖	CompOp	96 math math: TensorAlgebra.ofDirectSum_of_tprod, SymmetricAlgebra.lift_ι_apply, SymmetricAlgebra.rank_eq, SymmetricAlgebra.isSymmetricAlgebra_ι, CliffordAlgebra.involute_prod_map_ι, TensorAlgebra.toTrivSqZeroExt_ι, TensorAlgebra.ι_comp_lift, TensorAlgebra.adjoin_range_ι, TensorAlgebra.toDirectSum_tensorPower_tprod, IsSymmetricAlgebra.equiv_apply, CliffordAlgebra.contractRight_mul_ι, TensorAlgebra.ι_def, CliffordAlgebra.changeFormAux_changeFormAux, TensorAlgebra.instIsDomain, CliffordAlgebra.EquivEven.ι_eq_v_add_smul_e0, CliffordAlgebra.foldr'Aux_foldr'Aux, TensorAlgebra.toDirectSum_ofDirectSum, SymmetricAlgebra.instModuleFree, TensorAlgebra.toExterior_ι, TensorAlgebra.equivFreeAlgebra_symm_ι, LinearAlgebra.FreeProduct.ι_apply, TensorAlgebra.lift_symm_apply, TensorAlgebra.equivDirectSum_apply, TensorAlgebra.equivFreeAlgebra_ι_apply, TensorAlgebra.lift_ι_apply, TensorAlgebra.instModuleFree, TensorAlgebra.rank_eq, spinGroup.conjAct_smul_range_ι, IsSymmetricAlgebra.equiv_symm_comp, TensorAlgebra.toClifford_ι, TensorAlgebra.lift_comp_ι, CliffordAlgebra.submodule_comap_mul_reverse, TensorAlgebra.ι_range_disjoint_one, CliffordAlgebra.submodule_map_pow_reverse, TensorAlgebra.instNoZeroDivisors, CliffordAlgebra.contractLeft_ι_mul, CliffordAlgebra.star_smul, SymmetricAlgebra.algebraMap_eq_zero_iff, TensorAlgebra.ofDirectSum_toDirectSum, FreeAlgebra.toTensor_ι, IsSymmetricAlgebra.equiv_symm_apply, TensorAlgebra.instNontrivial, TensorAlgebra.algebraMap_eq_one_iff, CliffordAlgebraQuaternion.ofQuaternion_mk, pinGroup.conjAct_smul_range_ι, TensorPower.toTensorAlgebra_gMul, TensorPower.toTensorAlgebra_gOne, SymmetricAlgebra.algHom_ext_iff, SymmetricAlgebra.equivMvPolynomial_symm_X, SymmetricAlgebra.lift_comp_ι, SymmetricAlgebra.lift_ι, Module.Basis.symmetricAlgebra_repr_apply, SymmetricAlgebra.instIsDomain, TensorAlgebra.toDirectSum_comp_ofDirectSum, SymmetricAlgebra.equivMvPolynomial_ι_apply, TensorAlgebra.ι_leftInverse, UniversalEnvelopingAlgebra.ι_apply, TensorAlgebra.GradedAlgebra.ι_apply, TensorAlgebra.hom_ext_iff, TensorAlgebra.range_lift, SymmetricAlgebra.algebraMap_eq_one_iff, LinearAlgebra.FreeProduct.rel_id, TensorAlgebra.algebraMap_inj, Module.Basis.tensorAlgebra_repr_apply, TensorAlgebra.tprod_apply, CliffordAlgebra.submodule_map_mul_reverse, CliffordAlgebra.evenOdd_mul_le, instIsScalarTowerTensorAlgebra, TensorAlgebra.equivDirectSum_symm_apply, SymmetricAlgebra.algHom_surjective, TensorAlgebra.ι_inj, CliffordAlgebra.iSup_ι_range_eq_top, TensorAlgebra.ι_eq_zero_iff, CliffordAlgebra.submodule_comap_pow_reverse, SymmetricAlgebra.algebraMap_leftInverse, TensorAlgebra.algebraMap_leftInverse, SymmetricAlgebra.algebraMap_inj, LinearAlgebra.FreeProduct.lift_apply, IsSymmetricAlgebra.comp_equiv, TensorPower.toTensorAlgebra_galgebra_toFun, TensorAlgebra.algebraMap_eq_zero_iff, TensorAlgebra.toDirectSum_ι, ExteriorAlgebra.ιMulti_succ_curryLeft, TensorAlgebra.lift_unique, TensorAlgebra.ofDirectSum_comp_toDirectSum, SymmetricAlgebra.instNoZeroDivisors, IsSymmetricAlgebra.equiv_toAlgHom, TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι, ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot, instSMulCommClassTensorAlgebra, TensorAlgebra.ι_eq_algebraMap_iff, exteriorPower.zeroEquiv_symm_apply, TensorPower.toTensorAlgebra_tprod, CliffordAlgebra.contractLeftAux_contractLeftAux, lipschitzGroup.conjAct_smul_range_ι, UniversalEnvelopingAlgebra.lift_ι_apply'
instAlgebra 📖	CompOp	71 math math: TensorAlgebra.ofDirectSum_of_tprod, SymmetricAlgebra.lift_ι_apply, SymmetricAlgebra.rank_eq, SymmetricAlgebra.isSymmetricAlgebra_ι, TensorAlgebra.toTrivSqZeroExt_ι, TensorAlgebra.ι_comp_lift, TensorAlgebra.adjoin_range_ι, TensorAlgebra.toDirectSum_tensorPower_tprod, IsSymmetricAlgebra.equiv_apply, TensorAlgebra.ι_def, TensorAlgebra.toDirectSum_ofDirectSum, SymmetricAlgebra.instModuleFree, TensorAlgebra.toExterior_ι, TensorAlgebra.equivFreeAlgebra_symm_ι, LinearAlgebra.FreeProduct.ι_apply, TensorAlgebra.lift_symm_apply, TensorAlgebra.equivDirectSum_apply, TensorAlgebra.equivFreeAlgebra_ι_apply, TensorAlgebra.lift_ι_apply, TensorAlgebra.instModuleFree, TensorAlgebra.rank_eq, IsSymmetricAlgebra.equiv_symm_comp, TensorAlgebra.toClifford_ι, TensorAlgebra.lift_comp_ι, TensorAlgebra.ι_range_disjoint_one, SymmetricAlgebra.algebraMap_eq_zero_iff, TensorAlgebra.ofDirectSum_toDirectSum, FreeAlgebra.toTensor_ι, IsSymmetricAlgebra.equiv_symm_apply, TensorAlgebra.algebraMap_eq_one_iff, TensorPower.toTensorAlgebra_gMul, TensorPower.toTensorAlgebra_gOne, SymmetricAlgebra.algHom_ext_iff, SymmetricAlgebra.equivMvPolynomial_symm_X, SymmetricAlgebra.lift_comp_ι, SymmetricAlgebra.lift_ι, Module.Basis.symmetricAlgebra_repr_apply, TensorAlgebra.toDirectSum_comp_ofDirectSum, SymmetricAlgebra.equivMvPolynomial_ι_apply, TensorAlgebra.ι_leftInverse, UniversalEnvelopingAlgebra.ι_apply, TensorAlgebra.GradedAlgebra.ι_apply, TensorAlgebra.hom_ext_iff, TensorAlgebra.range_lift, SymmetricAlgebra.algebraMap_eq_one_iff, LinearAlgebra.FreeProduct.rel_id, TensorAlgebra.algebraMap_inj, Module.Basis.tensorAlgebra_repr_apply, TensorAlgebra.tprod_apply, instIsScalarTowerTensorAlgebra, TensorAlgebra.equivDirectSum_symm_apply, SymmetricAlgebra.algHom_surjective, TensorAlgebra.ι_inj, TensorAlgebra.ι_eq_zero_iff, SymmetricAlgebra.algebraMap_leftInverse, TensorAlgebra.algebraMap_leftInverse, SymmetricAlgebra.algebraMap_inj, LinearAlgebra.FreeProduct.lift_apply, IsSymmetricAlgebra.comp_equiv, TensorPower.toTensorAlgebra_galgebra_toFun, TensorAlgebra.algebraMap_eq_zero_iff, TensorAlgebra.toDirectSum_ι, TensorAlgebra.lift_unique, TensorAlgebra.ofDirectSum_comp_toDirectSum, IsSymmetricAlgebra.equiv_toAlgHom, TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι, ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot, instSMulCommClassTensorAlgebra, TensorAlgebra.ι_eq_algebraMap_iff, TensorPower.toTensorAlgebra_tprod, UniversalEnvelopingAlgebra.lift_ι_apply'
instInhabitedTensorAlgebra 📖	CompOp	—
instSemiringTensorAlgebra 📖	CompOp	98 math math: TensorAlgebra.ofDirectSum_of_tprod, SymmetricAlgebra.lift_ι_apply, SymmetricAlgebra.rank_eq, SymmetricAlgebra.isSymmetricAlgebra_ι, CliffordAlgebra.involute_prod_map_ι, TensorAlgebra.toTrivSqZeroExt_ι, TensorAlgebra.ι_comp_lift, TensorAlgebra.adjoin_range_ι, TensorAlgebra.toDirectSum_tensorPower_tprod, IsSymmetricAlgebra.equiv_apply, LinearAlgebra.FreeProduct.mul_injections, CliffordAlgebra.contractRight_mul_ι, TensorAlgebra.ι_def, CliffordAlgebra.changeFormAux_changeFormAux, TensorAlgebra.instIsDomain, CliffordAlgebra.EquivEven.ι_eq_v_add_smul_e0, CliffordAlgebra.foldr'Aux_foldr'Aux, TensorAlgebra.toDirectSum_ofDirectSum, SymmetricAlgebra.instModuleFree, TensorAlgebra.toExterior_ι, TensorAlgebra.equivFreeAlgebra_symm_ι, LinearAlgebra.FreeProduct.ι_apply, TensorAlgebra.lift_symm_apply, TensorAlgebra.equivDirectSum_apply, TensorAlgebra.equivFreeAlgebra_ι_apply, TensorAlgebra.lift_ι_apply, TensorAlgebra.instModuleFree, TensorAlgebra.rank_eq, spinGroup.conjAct_smul_range_ι, IsSymmetricAlgebra.equiv_symm_comp, TensorAlgebra.toClifford_ι, TensorAlgebra.lift_comp_ι, CliffordAlgebra.submodule_comap_mul_reverse, TensorAlgebra.ι_range_disjoint_one, CliffordAlgebra.submodule_map_pow_reverse, TensorAlgebra.instNoZeroDivisors, CliffordAlgebra.contractLeft_ι_mul, CliffordAlgebra.star_smul, SymmetricAlgebra.algebraMap_eq_zero_iff, LinearAlgebra.FreeProduct.identify_one, TensorAlgebra.ofDirectSum_toDirectSum, FreeAlgebra.toTensor_ι, IsSymmetricAlgebra.equiv_symm_apply, TensorAlgebra.algebraMap_eq_one_iff, CliffordAlgebraQuaternion.ofQuaternion_mk, pinGroup.conjAct_smul_range_ι, TensorPower.toTensorAlgebra_gMul, TensorPower.toTensorAlgebra_gOne, SymmetricAlgebra.algHom_ext_iff, SymmetricAlgebra.equivMvPolynomial_symm_X, SymmetricAlgebra.lift_comp_ι, SymmetricAlgebra.lift_ι, Module.Basis.symmetricAlgebra_repr_apply, SymmetricAlgebra.instIsDomain, TensorAlgebra.toDirectSum_comp_ofDirectSum, SymmetricAlgebra.equivMvPolynomial_ι_apply, TensorAlgebra.ι_leftInverse, UniversalEnvelopingAlgebra.ι_apply, TensorAlgebra.GradedAlgebra.ι_apply, TensorAlgebra.hom_ext_iff, TensorAlgebra.range_lift, SymmetricAlgebra.algebraMap_eq_one_iff, LinearAlgebra.FreeProduct.rel_id, TensorAlgebra.algebraMap_inj, Module.Basis.tensorAlgebra_repr_apply, TensorAlgebra.tprod_apply, CliffordAlgebra.submodule_map_mul_reverse, CliffordAlgebra.evenOdd_mul_le, instIsScalarTowerTensorAlgebra, TensorAlgebra.equivDirectSum_symm_apply, SymmetricAlgebra.algHom_surjective, TensorAlgebra.ι_inj, CliffordAlgebra.iSup_ι_range_eq_top, TensorAlgebra.ι_eq_zero_iff, CliffordAlgebra.submodule_comap_pow_reverse, SymmetricAlgebra.algebraMap_leftInverse, TensorAlgebra.algebraMap_leftInverse, SymmetricAlgebra.algebraMap_inj, LinearAlgebra.FreeProduct.lift_apply, IsSymmetricAlgebra.comp_equiv, TensorPower.toTensorAlgebra_galgebra_toFun, TensorAlgebra.algebraMap_eq_zero_iff, TensorAlgebra.toDirectSum_ι, ExteriorAlgebra.ιMulti_succ_curryLeft, TensorAlgebra.lift_unique, TensorAlgebra.ofDirectSum_comp_toDirectSum, SymmetricAlgebra.instNoZeroDivisors, IsSymmetricAlgebra.equiv_toAlgHom, TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι, ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot, LinearAlgebra.FreeProduct.lof_map_one, instSMulCommClassTensorAlgebra, TensorAlgebra.ι_eq_algebraMap_iff, exteriorPower.zeroEquiv_symm_apply, TensorPower.toTensorAlgebra_tprod, CliffordAlgebra.contractLeftAux_contractLeftAux, lipschitzGroup.conjAct_smul_range_ι, UniversalEnvelopingAlgebra.lift_ι_apply'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsScalarTowerTensorAlgebra 📖	mathematical	—	IsScalarTower TensorAlgebra Algebra.toSMul instSemiringTensorAlgebra instAlgebra	—	RingQuot.instIsScalarTower FreeAlgebra.instIsScalarTower
instSMulCommClassTensorAlgebra 📖	mathematical	—	SMulCommClass TensorAlgebra Algebra.toSMul instSemiringTensorAlgebra instAlgebra	—	RingQuot.instSMulCommClass FreeAlgebra.instSMulCommClass

---

← Back to Index