Quotient

📁 Source: Mathlib/LinearAlgebra/TensorProduct/Quotient.lean

Statistics

Metric	Count
Definitions qoutMapEquivTensorQout, tensorQuotientEquiv, quotTensorEquivQuotSMul, quotientTensorEquiv, quotientTensorQuotientEquiv, tensorQuotEquivQuotSMul, tensorQuotMapSMulEquivTensorQuot, tensorQuotientEquiv	8
Theorems ker_mapOfCompatibleSMul, tensorQuotientEquiv_apply_tmul, tensorQuotientEquiv_symm_apply_mk_tmul, quotTensorEquivQuotSMul_comp_mk, quotTensorEquivQuotSMul_comp_mkQ_rTensor, quotTensorEquivQuotSMul_mk_one_tmul, quotTensorEquivQuotSMul_mk_tmul, quotTensorEquivQuotSMul_symm_comp_mkQ, quotTensorEquivQuotSMul_symm_mk, quotientTensorEquiv_apply_tmul_mk, quotientTensorEquiv_symm_apply_mk_tmul, quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, quotientTensorQuotientEquiv_symm_apply_mk_tmul, tensorQuotEquivQuotSMul_comp_mk, tensorQuotEquivQuotSMul_comp_mkQ_lTensor, tensorQuotEquivQuotSMul_symm_comp_mkQ, tensorQuotEquivQuotSMul_symm_mk, tensorQuotEquivQuotSMul_tmul_mk, tensorQuotientEquiv_apply_mk_tmul, tensorQuotientEquiv_symm_apply_tmul_mk	20
Total	28

Ideal

Definitions

Name	Category	Theorems
qoutMapEquivTensorQout 📖	CompOp	—

TensorProduct

Definitions

Name	Category	Theorems
quotTensorEquivQuotSMul 📖	CompOp	6 math math: quotTensorEquivQuotSMul_comp_mkQ_rTensor, quotTensorEquivQuotSMul_mk_one_tmul, quotTensorEquivQuotSMul_symm_mk, quotTensorEquivQuotSMul_comp_mk, quotTensorEquivQuotSMul_symm_comp_mkQ, quotTensorEquivQuotSMul_mk_tmul
quotientTensorEquiv 📖	CompOp	2 math math: quotientTensorEquiv_symm_apply_mk_tmul, quotientTensorEquiv_apply_tmul_mk
quotientTensorQuotientEquiv 📖	CompOp	2 math math: quotientTensorQuotientEquiv_symm_apply_mk_tmul, quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk
tensorQuotEquivQuotSMul 📖	CompOp	5 math math: tensorQuotEquivQuotSMul_comp_mkQ_lTensor, tensorQuotEquivQuotSMul_tmul_mk, tensorQuotEquivQuotSMul_symm_mk, tensorQuotEquivQuotSMul_comp_mk, tensorQuotEquivQuotSMul_symm_comp_mkQ
tensorQuotMapSMulEquivTensorQuot 📖	CompOp	—
tensorQuotientEquiv 📖	CompOp	2 math math: tensorQuotientEquiv_apply_mk_tmul, tensorQuotientEquiv_symm_apply_tmul_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotTensorEquivQuotSMul_comp_mk 📖	mathematical	—	LinearMap.comp TensorProduct CommRing.toCommSemiring HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing AddCommGroup.toAddCommMonoid Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Submodule Ring.toSemiring Submodule.hasQuotient Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop addCommMonoid Submodule.Quotient.addCommGroup instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids quotTensorEquivQuotSMul DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_left smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid LinearMap.instFunLike Ideal.Quotient.one Submodule.mkQ	—	IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_left smulCommClass_self LinearEquiv.toLinearMap_symm_comp_eq quotTensorEquivQuotSMul_symm_comp_mkQ
quotTensorEquivQuotSMul_comp_mkQ_rTensor 📖	mathematical	—	LinearMap.comp TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring HasQuotient.Quotient Submodule Ring.toSemiring Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module Ideal Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing quotTensorEquivQuotSMul LinearMap.rTensor Submodule.mkQ NonAssocSemiring.toNonUnitalNonAssocSemiring lid	—	ext' IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids quotTensorEquivQuotSMul_mk_tmul
quotTensorEquivQuotSMul_mk_one_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing AddCommGroup.toAddCommMonoid Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Submodule Submodule.hasQuotient Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop addCommMonoid Submodule.Quotient.addCommGroup instModule EquivLike.toFunLike LinearEquiv.instEquivLike quotTensorEquivQuotSMul tmul Ideal.Quotient.one	—	IsScalarTower.left RingHomInvPair.ids Ideal.instIsTwoSided_1 RingHom.map_one quotTensorEquivQuotSMul_mk_tmul one_smul
quotTensorEquivQuotSMul_mk_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing AddCommGroup.toAddCommMonoid Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Submodule Submodule.hasQuotient Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop addCommMonoid Submodule.Quotient.addCommGroup instModule EquivLike.toFunLike LinearEquiv.instEquivLike quotTensorEquivQuotSMul tmul RingHom Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	Ideal.instIsTwoSided_1 RingHomInvPair.ids IsScalarTower.left LinearEquiv.eq_symm_apply IsScalarTower.right smul_eq_mul mul_one Submodule.Quotient.mk_smul smul_tmul CompatibleSMul.isScalarTower Submodule.Quotient.isScalarTower
quotTensorEquivQuotSMul_symm_comp_mkQ 📖	mathematical	—	LinearMap.comp HasQuotient.Quotient Submodule Ring.toSemiring CommRing.toRing AddCommGroup.toAddCommMonoid Submodule.hasQuotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop TensorProduct Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module Ring.toAddCommGroup Submodule.Quotient.addCommGroup addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm quotTensorEquivQuotSMul Submodule.mkQ DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_left smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid LinearMap.instFunLike Ideal.Quotient.one	—	LinearMap.ext IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids smulCommClass_left smulCommClass_self
quotTensorEquivQuotSMul_symm_mk 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop TensorProduct Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module Ring.toAddCommGroup Submodule.Quotient.addCommGroup addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotTensorEquivQuotSMul tmul Ideal.Quotient.one	—	RingHomInvPair.ids IsScalarTower.left
quotientTensorEquiv_apply_tmul_mk 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.Quotient.addCommGroup Submodule.Quotient.module addCommMonoid instModule addCommGroup LinearMap.range SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHomSurjective.ids map Submodule.subtype LinearMap.id EquivLike.toFunLike LinearEquiv.instEquivLike quotientTensorEquiv tmul	—	RingHomSurjective.ids RingHomInvPair.ids
quotientTensorEquiv_symm_apply_mk_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient TensorProduct AddCommGroup.toAddCommMonoid Submodule addCommMonoid instModule Submodule.hasQuotient CommRing.toRing addCommGroup LinearMap.range SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHomSurjective.ids map Submodule.subtype LinearMap.id Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotientTensorEquiv tmul Ring.toSemiring	—	RingHomInvPair.ids RingHomSurjective.ids
quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.Quotient.addCommGroup Submodule.Quotient.module addCommMonoid instModule addCommGroup SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice LinearMap.range SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHomSurjective.ids map Submodule.subtype LinearMap.id EquivLike.toFunLike LinearEquiv.instEquivLike quotientTensorQuotientEquiv tmul	—	RingHomSurjective.ids RingHomInvPair.ids
quotientTensorQuotientEquiv_symm_apply_mk_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient TensorProduct AddCommGroup.toAddCommMonoid Submodule addCommMonoid instModule Submodule.hasQuotient CommRing.toRing addCommGroup SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice LinearMap.range SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHomSurjective.ids map Submodule.subtype LinearMap.id Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotientTensorQuotientEquiv tmul Ring.toSemiring	—	RingHomInvPair.ids RingHomSurjective.ids
tensorQuotEquivQuotSMul_comp_mk 📖	mathematical	—	LinearMap.comp TensorProduct CommRing.toCommSemiring HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Submodule Ring.toSemiring Submodule.hasQuotient Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop addCommMonoid Submodule.Quotient.addCommGroup instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids tensorQuotEquivQuotSMul DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul smulCommClass_left smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid LinearMap.instFunLike LinearMap.flip Ideal.Quotient.one Submodule.mkQ	—	IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids SMulCommClass.symm smulCommClass_left smulCommClass_self LinearEquiv.toLinearMap_symm_comp_eq tensorQuotEquivQuotSMul_symm_comp_mkQ
tensorQuotEquivQuotSMul_comp_mkQ_lTensor 📖	mathematical	—	LinearMap.comp TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring HasQuotient.Quotient Submodule Ring.toSemiring Submodule.hasQuotient Submodule.Quotient.addCommGroup Submodule.Quotient.module Ideal Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing tensorQuotEquivQuotSMul LinearMap.lTensor Submodule.mkQ NonAssocSemiring.toNonUnitalNonAssocSemiring rid	—	ext' IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids
tensorQuotEquivQuotSMul_symm_comp_mkQ 📖	mathematical	—	LinearMap.comp HasQuotient.Quotient Submodule Ring.toSemiring CommRing.toRing AddCommGroup.toAddCommMonoid Submodule.hasQuotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop TensorProduct Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module Ring.toAddCommGroup Submodule.Quotient.addCommGroup addCommMonoid instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm tensorQuotEquivQuotSMul Submodule.mkQ DFunLike.coe LinearMap LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul smulCommClass_left smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid LinearMap.instFunLike LinearMap.flip Ideal.Quotient.one	—	LinearMap.ext IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids SMulCommClass.symm smulCommClass_left smulCommClass_self
tensorQuotEquivQuotSMul_symm_mk 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop TensorProduct Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module Ring.toAddCommGroup Submodule.Quotient.addCommGroup addCommMonoid instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm tensorQuotEquivQuotSMul tmul Ideal.Quotient.one	—	RingHomInvPair.ids IsScalarTower.left
tensorQuotEquivQuotSMul_tmul_mk 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Submodule Submodule.hasQuotient Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Top.top Submodule.instTop addCommMonoid Submodule.Quotient.addCommGroup instModule EquivLike.toFunLike LinearEquiv.instEquivLike tensorQuotEquivQuotSMul tmul RingHom Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	quotTensorEquivQuotSMul_mk_tmul
tensorQuotientEquiv_apply_mk_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.Quotient.addCommGroup Submodule.Quotient.module addCommMonoid instModule addCommGroup LinearMap.range SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHomSurjective.ids map LinearMap.id Submodule.subtype EquivLike.toFunLike LinearEquiv.instEquivLike tensorQuotientEquiv tmul	—	RingHomSurjective.ids RingHomInvPair.ids
tensorQuotientEquiv_symm_apply_tmul_mk 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient TensorProduct AddCommGroup.toAddCommMonoid Submodule addCommMonoid instModule Submodule.hasQuotient CommRing.toRing addCommGroup LinearMap.range SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHomSurjective.ids map LinearMap.id Submodule.subtype Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm tensorQuotientEquiv tmul Ring.toSemiring	—	RingHomInvPair.ids RingHomSurjective.ids

TensorProduct.AlgebraTensorModule

Definitions

Name	Category	Theorems
tensorQuotientEquiv 📖	CompOp	2 math math: tensorQuotientEquiv_symm_apply_mk_tmul, tensorQuotientEquiv_apply_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_mapOfCompatibleSMul 📖	mathematical	—	LinearMap.ker TensorProduct CommRing.toCommSemiring AddCommGroup.toAddCommMonoid CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring TensorProduct.mapOfCompatibleSMul IsScalarTower.to_smulCommClass' TensorProduct.CompatibleSMul.isScalarTower MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.toSMul Submodule.span setOf SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup TensorProduct.addCommGroup TensorProduct.tmul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	IsScalarTower.to_smulCommClass smulCommClass_self IsScalarTower.to_smulCommClass' TensorProduct.CompatibleSMul.isScalarTower Submodule.span_eq_of_le map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass TensorProduct.smul_tmul IsScalarTower.left TensorProduct.tmul_smul sub_self TensorProduct.tmul_add Submodule.mkQ_apply Submodule.Quotient.mk_smul Submodule.Quotient.eq RingHom.id_apply Submodule.subset_span LinearMap.ext TensorProduct.add_tmul RingHomCompTriple.ids curry_injective TensorProduct.isScalarTower_left Submodule.Quotient.isScalarTower Submodule.ker_mkQ LinearMap.ker_le_ker_comp
tensorQuotientEquiv_apply_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Submodule.Quotient.addCommGroup Submodule.Quotient.module' Algebra.toSMul TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass TensorProduct.addCommGroup LinearMap.range SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module' RingHomSurjective.ids LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' LinearMap.instFunLike lTensor LinearMap.restrictScalars Submodule.module LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Submodule.isScalarTower' AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.subtype Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike tensorQuotientEquiv TensorProduct.tmul	—	IsScalarTower.to_smulCommClass RingHomSurjective.ids smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' LinearMap.IsScalarTower.compatibleSMul Submodule.isScalarTower' RingHomInvPair.ids
tensorQuotientEquiv_symm_apply_mk_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient TensorProduct AddCommGroup.toAddCommMonoid Submodule TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass Submodule.hasQuotient CommRing.toRing TensorProduct.addCommGroup LinearMap.range SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module' Algebra.toSMul RingHomSurjective.ids LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction TensorProduct.instModule TensorProduct.smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsScalarTower.to_smulCommClass' LinearMap.instFunLike lTensor LinearMap.restrictScalars Submodule.module LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Submodule.isScalarTower' AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring Submodule.subtype Submodule.Quotient.addCommGroup Submodule.Quotient.module' Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm tensorQuotientEquiv TensorProduct.tmul Ring.toSemiring	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass RingHomSurjective.ids smulCommClass_self TensorProduct.smulCommClass_left IsScalarTower.to_smulCommClass' LinearMap.IsScalarTower.compatibleSMul Submodule.isScalarTower'

---

← Back to Index