Quotient

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

Statistics

Metric	Count
Definitions qoutMapEquivTensorQout, quotTensorEquivQuotSMul, quotientTensorEquiv, quotientTensorQuotientEquiv, tensorQuotEquivQuotSMul, tensorQuotMapSMulEquivTensorQuot, tensorQuotientEquiv	7
Theorems quotTensorEquivQuotSMul_comp_mk, quotTensorEquivQuotSMul_comp_mkQ_rTensor, 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	16
Total	23

Ideal

Definitions

Name	Category	Theorems
qoutMapEquivTensorQout 📖	CompOp	—

TensorProduct

Definitions

Name	Category	Theorems
quotTensorEquivQuotSMul 📖	CompOp	5 math math: quotTensorEquivQuotSMul_comp_mkQ_rTensor, 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_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

---

← Back to Index