MvPolynomial

📁 Source: Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

Statistics

Metric	Count
Definitions algebraTensorAlgEquiv, rTensor, rTensorAlgEquiv, rTensorAlgHom, scalarRTensor, scalarRTensorAlgEquiv, tensorEquivSum	7
Theorems aeval_one_tmul, algebraTensorAlgEquiv_symm_X, algebraTensorAlgEquiv_symm_comp_aeval, algebraTensorAlgEquiv_symm_map, algebraTensorAlgEquiv_symm_monomial, algebraTensorAlgEquiv_tmul, coeff_rTensorAlgHom_monomial_tmul, coeff_rTensorAlgHom_tmul, instIsPushout, instIsPushout_1, rTensorAlgEquiv_apply, rTensorAlgHom_apply_eq, rTensorAlgHom_toLinearMap, rTensor_apply, rTensor_apply_X_tmul, rTensor_apply_monomial_tmul, rTensor_apply_tmul, rTensor_apply_tmul_apply, rTensor_symm_apply_single, scalarRTensor_apply_X_tmul_apply, scalarRTensor_apply_monomial_tmul, scalarRTensor_apply_tmul, scalarRTensor_apply_tmul_apply, scalarRTensor_symm_apply_single, tensorEquivSum_C_tmul_C, tensorEquivSum_C_tmul_one, tensorEquivSum_X_tmul_X, tensorEquivSum_X_tmul_one, tensorEquivSum_one_tmul_C, tensorEquivSum_one_tmul_X	30
Total	37

MvPolynomial

Definitions

Name	Category	Theorems
algebraTensorAlgEquiv 📖	CompOp	6 math math: algebraTensorAlgEquiv_symm_comp_aeval, algebraTensorAlgEquiv_symm_X, algebraTensorAlgEquiv_symm_map, Algebra.Presentation.algebraTensorAlgEquiv_symm_relation, algebraTensorAlgEquiv_tmul, algebraTensorAlgEquiv_symm_monomial
rTensor 📖	CompOp	8 math math: rTensor_apply_tmul_apply, rTensor_apply_X_tmul, rTensor_apply_tmul, rTensorAlgHom_toLinearMap, rTensor_symm_apply_single, rTensor_apply_monomial_tmul, rTensor_apply, rTensorAlgHom_apply_eq
rTensorAlgEquiv 📖	CompOp	1 math math: rTensorAlgEquiv_apply
rTensorAlgHom 📖	CompOp	5 math math: rTensorAlgEquiv_apply, rTensorAlgHom_toLinearMap, coeff_rTensorAlgHom_tmul, coeff_rTensorAlgHom_monomial_tmul, rTensorAlgHom_apply_eq
scalarRTensor 📖	CompOp	5 math math: scalarRTensor_apply_monomial_tmul, scalarRTensor_apply_X_tmul_apply, scalarRTensor_apply_tmul, scalarRTensor_symm_apply_single, scalarRTensor_apply_tmul_apply
scalarRTensorAlgEquiv 📖	CompOp	—
tensorEquivSum 📖	CompOp	11 math math: tensorEquivSum_one_tmul_C, universalFactorizationMapPresentation_relation, ker_eval₂Hom_universalFactorizationMap, tensorEquivSum_X_tmul_X, tensorEquivSum_C_tmul_one, pderiv_inr_universalFactorizationMap_X, tensorEquivSum_one_tmul_X, universalFactorizationMapPresentation_σ', tensorEquivSum_X_tmul_one, tensorEquivSum_C_tmul_C, pderiv_inl_universalFactorizationMap_X

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_one_tmul 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule commSemiring Algebra.TensorProduct.instCommSemiring algebra Algebra.id Algebra.TensorProduct.instAlgebra AlgHom.funLike aeval TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	induction_on algHom_C mul_one Algebra.smul_def TensorProduct.smul_tmul TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left map_add SemilinearMapClass.toAddHomClass Algebra.to_smulCommClass IsScalarTower.right NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass TensorProduct.tmul_add map_mul NonUnitalAlgSemiHomClass.toMulHomClass aeval_X
algebraTensorAlgEquiv_symm_X 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Algebra.toModule module Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm algebraTensorAlgEquiv X TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Algebra.to_smulCommClass aeval_X
algebraTensorAlgEquiv_symm_comp_aeval 📖	mathematical	—	AlgHom.comp MvPolynomial TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Algebra.toModule module Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.instAlgebra AlgHomClass.toAlgHom AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass AlgEquiv.restrictScalars Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass isScalarTower Algebra.toSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.right TensorProduct.isScalarTower_left AlgEquiv.symm algebraTensorAlgEquiv mapAlgHom Algebra.ofId Algebra.TensorProduct.includeRight	—	algHom_ext AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Algebra.to_smulCommClass isScalarTower IsScalarTower.right TensorProduct.isScalarTower_left eval₂_X algebraTensorAlgEquiv_symm_X
algebraTensorAlgEquiv_symm_map 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Algebra.toModule module Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm algebraTensorAlgEquiv RingHom RingHom.instFunLike map algebraMap TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	DFunLike.congr_fun AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Algebra.to_smulCommClass isScalarTower IsScalarTower.right TensorProduct.isScalarTower_left algebraTensorAlgEquiv_symm_comp_aeval
algebraTensorAlgEquiv_symm_monomial 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Algebra.toModule module Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm algebraTensorAlgEquiv LinearMap RingHom.id LinearMap.instFunLike monomial TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Finsupp.induction Algebra.to_smulCommClass algHom_C IsScalarTower.right add_comm monomial_add_single map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass aeval_X Algebra.TensorProduct.tmul_pow one_pow mul_one Algebra.TensorProduct.tmul_mul_tmul
algebraTensorAlgEquiv_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring Algebra.toModule module Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike algebraTensorAlgEquiv TensorProduct.tmul Algebra.toSMul RingHom RingHom.instFunLike map algebraMap	—	Algebra.to_smulCommClass Algebra.smul_def
coeff_rTensorAlgHom_monomial_tmul 📖	mathematical	—	coeff TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Algebra.TensorProduct.instCommSemiring DFunLike.coe AlgHom MvPolynomial commSemiring module Algebra.TensorProduct.instSemiring algebra Algebra.TensorProduct.leftAlgebra Algebra.id smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgHom.funLike rTensorAlgHom TensorProduct.tmul LinearMap RingHom.id Semiring.toModule LinearMap.instFunLike monomial Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instDecidableEq TensorProduct.zero	—	smulCommClass Algebra.to_smulCommClass coeff_rTensorAlgHom_tmul coeff_monomial TensorProduct.ite_tmul
coeff_rTensorAlgHom_tmul 📖	mathematical	—	coeff TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule Algebra.TensorProduct.instCommSemiring DFunLike.coe AlgHom MvPolynomial commSemiring module Algebra.TensorProduct.instSemiring algebra Algebra.TensorProduct.leftAlgebra Algebra.id smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgHom.funLike rTensorAlgHom TensorProduct.tmul	—	smulCommClass Algebra.to_smulCommClass rTensorAlgHom.eq_1 IsScalarTower.to_smulCommClass Algebra.TensorProduct.lift_tmul AlgHom.coe_comp IsScalarTower.coe_toAlgHom' Algebra.TensorProduct.includeRight_apply algebraMap_eq mul_comm coeff_C_mul coeff_map one_mul mul_one
instIsPushout 📖	mathematical	—	Algebra.IsPushout MvPolynomial commSemiring algebra Algebra.id algebraMvPolynomial instIsScalarTower isScalarTower Algebra.toSMul CommSemiring.toSemiring DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right	—	instIsScalarTower isScalarTower IsScalarTower.right IsBaseChange.of_equiv Algebra.to_smulCommClass RingHomInvPair.ids algebraTensorAlgEquiv_tmul Algebra.smul_def one_mul
instIsPushout_1 📖	mathematical	—	Algebra.IsPushout MvPolynomial commSemiring algebra Algebra.id algebraMvPolynomial isScalarTower Algebra.toSMul CommSemiring.toSemiring DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule IsScalarTower.right instIsScalarTower	—	Algebra.IsPushout.symm instIsScalarTower isScalarTower IsScalarTower.right instIsPushout
rTensorAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring module Algebra.toModule Algebra.TensorProduct.instCommSemiring Algebra.TensorProduct.instSemiring algebra Algebra.TensorProduct.leftAlgebra Algebra.id smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgEquiv.instFunLike rTensorAlgEquiv AlgHom AlgHom.funLike rTensorAlgHom	—	smulCommClass Algebra.to_smulCommClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgHom.coe_coe AlgEquiv.toAlgHom_eq_coe Algebra.TensorProduct.ext isScalarTower IsScalarTower.right TensorProduct.isScalarTower_left algHom_ext IsScalarTower.to_smulCommClass ext coeff_rTensorAlgHom_tmul rTensor_apply_tmul_apply AlgHom.ext
rTensorAlgHom_apply_eq 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring module Algebra.toModule Algebra.TensorProduct.instCommSemiring Algebra.TensorProduct.instSemiring algebra Algebra.TensorProduct.leftAlgebra Algebra.id smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgHom.funLike rTensorAlgHom LinearEquiv RingHom.id RingHomInvPair.ids Finsupp MulZeroClass.toZero Nat.instMulZeroClass TensorProduct.zero TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule instDistribSMul Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv rTensor	—	smulCommClass Algebra.to_smulCommClass RingHomInvPair.ids AlgHom.toLinearMap_apply rTensorAlgHom_toLinearMap
rTensorAlgHom_toLinearMap 📖	mathematical	—	AlgHom.toLinearMap TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring module Algebra.toModule Algebra.TensorProduct.instCommSemiring Algebra.TensorProduct.instSemiring algebra Algebra.TensorProduct.leftAlgebra Algebra.id smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass rTensorAlgHom LinearEquiv.toLinearMap RingHom.id RingHomInvPair.ids Finsupp MulZeroClass.toZero Nat.instMulZeroClass TensorProduct.zero TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule instDistribSMul Finsupp.module rTensor	—	TensorProduct.AlgebraTensorModule.curry_injective isScalarTower IsScalarTower.right Algebra.to_smulCommClass TensorProduct.isScalarTower_left smulCommClass RingHomInvPair.ids linearMap_ext IsScalarTower.to_smulCommClass LinearMap.ext_ring RingHomCompTriple.ids LinearMap.ext ext coeff_rTensorAlgHom_tmul Finsupp.smulCommClass TensorProduct.finsuppLeft_apply_tmul_apply
rTensor_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.zero Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids MvPolynomial commSemiring module TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instDistribSMul Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv rTensor LinearMap TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor LinearMap.restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddCommMonoid.toAddMonoid Algebra.toSMul isScalarTower IsScalarTower.right lcoeff	—	TensorProduct.finsuppLeft_apply
rTensor_apply_X_tmul 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.zero Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids MvPolynomial commSemiring module TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instDistribSMul Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv rTensor TensorProduct.tmul X Finsupp.single Finsupp.instDecidableEq AddMonoidWithOne.toOne	—	RingHomInvPair.ids smulCommClass Algebra.to_smulCommClass rTensor_apply_tmul_apply coeff_X' TensorProduct.ite_tmul
rTensor_apply_monomial_tmul 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.zero Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids MvPolynomial commSemiring module TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instDistribSMul Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv rTensor TensorProduct.tmul LinearMap LinearMap.instFunLike monomial Finsupp.instDecidableEq	—	RingHomInvPair.ids smulCommClass Algebra.to_smulCommClass rTensor_apply_tmul_apply coeff_monomial TensorProduct.ite_tmul
rTensor_apply_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring module Algebra.toModule Finsupp MulZeroClass.toZero Nat.instMulZeroClass TensorProduct.zero TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instDistribSMul Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv rTensor TensorProduct.tmul Finsupp.sum NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.single	—	TensorProduct.finsuppLeft_apply_tmul
rTensor_apply_tmul_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.zero Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids MvPolynomial commSemiring module TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instDistribSMul Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv rTensor TensorProduct.tmul coeff	—	TensorProduct.finsuppLeft_apply_tmul_apply
rTensor_symm_apply_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero Nat.instMulZeroClass TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.zero MvPolynomial commSemiring module Finsupp.instAddCommMonoid TensorProduct.addCommMonoid Finsupp.module TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instDistribSMul EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm rTensor Finsupp.single TensorProduct.tmul LinearMap LinearMap.instFunLike monomial	—	TensorProduct.finsuppLeft_symm_apply_single
scalarRTensor_apply_X_tmul_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring module Semiring.toModule TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv scalarRTensor TensorProduct.tmul X Finsupp.single Finsupp.instDecidableEq	—	RingHomInvPair.ids scalarRTensor_apply_tmul_apply coeff_X' ite_smul one_smul zero_smul
scalarRTensor_apply_monomial_tmul 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring module Semiring.toModule TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv scalarRTensor TensorProduct.tmul LinearMap LinearMap.instFunLike monomial Finsupp.instDecidableEq SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids scalarRTensor_apply_tmul_apply coeff_monomial ite_smul zero_smul
scalarRTensor_apply_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring module Semiring.toModule Finsupp MulZeroClass.toZero Nat.instMulZeroClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv scalarRTensor TensorProduct.tmul Finsupp.sum NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.single SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	TensorProduct.finsuppScalarLeft_apply_tmul
scalarRTensor_apply_tmul_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring module Semiring.toModule TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv scalarRTensor TensorProduct.tmul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction coeff	—	TensorProduct.finsuppScalarLeft_apply_tmul_apply
scalarRTensor_symm_apply_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero Nat.instMulZeroClass AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring commSemiring module Semiring.toModule Finsupp.instAddCommMonoid TensorProduct.addCommMonoid Finsupp.module TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm scalarRTensor Finsupp.single TensorProduct.tmul LinearMap LinearMap.instFunLike monomial AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	TensorProduct.finsuppScalarLeft_symm_apply_single
tensorEquivSum_C_tmul_C 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring module Algebra.toModule Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.leftAlgebra smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum TensorProduct.tmul RingHom RingHom.instFunLike C Algebra.toSMul	—	smulCommClass Algebra.to_smulCommClass algebraTensorAlgEquiv_tmul map_C Algebra.smul_def map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass iterToSum_C_C mul_comm NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass algHom_C C_mul
tensorEquivSum_C_tmul_one 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring module Algebra.toModule Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.leftAlgebra smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum TensorProduct.tmul RingHom RingHom.instFunLike C AddMonoidWithOne.toOne	—	smulCommClass Algebra.to_smulCommClass algebraTensorAlgEquiv_tmul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Algebra.smul_def mul_one iterToSum_C_C algHom_C
tensorEquivSum_X_tmul_X 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring module Algebra.toModule Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.leftAlgebra smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum TensorProduct.tmul X Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	smulCommClass Algebra.to_smulCommClass algebraTensorAlgEquiv_tmul map_X Algebra.smul_def map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass iterToSum_C_X iterToSum_X NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass rename_X
tensorEquivSum_X_tmul_one 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring module Algebra.toModule Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.leftAlgebra smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum TensorProduct.tmul X AddMonoidWithOne.toOne	—	smulCommClass Algebra.to_smulCommClass algebraTensorAlgEquiv_tmul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Algebra.smul_def mul_one iterToSum_C_X rename_X
tensorEquivSum_one_tmul_C 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring module Algebra.toModule Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.leftAlgebra smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum TensorProduct.tmul AddMonoidWithOne.toOne RingHom RingHom.instFunLike C algebraMap	—	smulCommClass Algebra.to_smulCommClass algebraTensorAlgEquiv_tmul map_C Algebra.smul_def one_mul iterToSum_C_C algHom_C
tensorEquivSum_one_tmul_X 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring module Algebra.toModule Semiring.toModule Algebra.TensorProduct.instSemiring algebra Algebra.id Algebra.TensorProduct.leftAlgebra smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum TensorProduct.tmul AddMonoidWithOne.toOne X	—	smulCommClass Algebra.to_smulCommClass algebraTensorAlgEquiv_tmul map_X Algebra.smul_def one_mul iterToSum_X rename_X

---

← Back to Index