Documentation Verification Report

Quotient

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

Statistics

Metric	Count
Definitions `quotIdealMapEquivTensorQuot`	1
Theorems `quotIdealMapEquivTensorQuot_mk`, `quotIdealMapEquivTensorQuot_symm_tmul`	2
Total	3

Algebra.TensorProduct

Definitions

Name	Category	Theorems
`quotIdealMapEquivTensorQuot` 📖	CompOp	2 math math: `quotIdealMapEquivTensorQuot_symm_tmul`, `quotIdealMapEquivTensorQuot_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`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`

---

← Back to Index