Quotient

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

Statistics

Metric	Count
Definitions quotIdealMapEquivQuotTensor, quotIdealMapEquivTensorQuot, tensorQuotientEquiv	3
Theorems quotIdealMapEquivQuotTensor_mk, quotIdealMapEquivTensorQuot_mk, quotIdealMapEquivTensorQuot_symm_tmul, tensorQuotientEquiv_apply_tmul, tensorQuotientEquiv_symm_apply_tmul	5
Total	8

Algebra.TensorProduct

Definitions

Name	Category	Theorems
quotIdealMapEquivQuotTensor 📖	CompOp	1 math math: quotIdealMapEquivQuotTensor_mk
quotIdealMapEquivTensorQuot 📖	CompOp	2 math math: quotIdealMapEquivTensorQuot_symm_tmul, quotIdealMapEquivTensorQuot_mk
tensorQuotientEquiv 📖	CompOp	2 math math: tensorQuotientEquiv_symm_apply_tmul, tensorQuotientEquiv_apply_tmul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotIdealMapEquivQuotTensor_mk 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toModule Ideal.Quotient.commSemiring Ideal.Quotient.semiring instSemiring Ideal.instAlgebraQuotient Algebra.id Ideal.Quotient.algebraQuotientMapQuotient leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike quotIdealMapEquivQuotTensor Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 TensorProduct.tmul Ideal.Quotient.one	—	Algebra.to_smulCommClass Ideal.instIsTwoSided_1
quotIdealMapEquivTensorQuot_mk 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Algebra.toModule Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Ideal.Quotient.semiring instSemiring Ideal.instAlgebraQuotient Algebra.id leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike quotIdealMapEquivTensorQuot Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 TensorProduct.tmul Ideal.Quotient.one	—	Algebra.to_smulCommClass Ideal.instIsTwoSided_1
quotIdealMapEquivTensorQuot_symm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct CommRing.toCommSemiring HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Algebra.toModule Submodule.Quotient.module CommRing.toRing Ring.toAddCommGroup Semiring.toModule Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap instSemiring Ideal.Quotient.semiring Ideal.instAlgebraQuotient Algebra.id leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm quotIdealMapEquivTensorQuot TensorProduct.tmul Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Algebra.toSMul	—	Algebra.to_smulCommClass Ideal.instIsTwoSided_1
tensorQuotientEquiv_apply_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct CommRing.toCommSemiring HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Algebra.toModule Submodule.Quotient.module' CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul IsScalarTower.right NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring instCommRing Ideal.map AlgHom instAlgebra AlgHom.funLike includeRight Ideal.Quotient.semiring Ideal.instAlgebraQuotient leftAlgebra IsScalarTower.to_smulCommClass AlgEquiv.instFunLike tensorQuotientEquiv TensorProduct.tmul RingHom Ring.toSemiring Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike instRing	—	IsScalarTower.right IsScalarTower.to_smulCommClass Ideal.instIsTwoSided_1
tensorQuotientEquiv_symm_apply_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Ideal NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring Ideal.instHasQuotient_1 instCommRing Ideal.map AlgHom instAlgebra AlgHom.funLike includeRight Ideal.Quotient.commRing Submodule.Quotient.module' CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul IsScalarTower.right Ideal.Quotient.semiring Ideal.instAlgebraQuotient leftAlgebra IsScalarTower.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm tensorQuotientEquiv RingHom Ring.toSemiring instRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike TensorProduct.tmul	—	IsScalarTower.right IsScalarTower.to_smulCommClass Ideal.instIsTwoSided_1

---

← Back to Index