Documentation Verification Report

ChineseRemainder

📁 Source: Mathlib/RingTheory/Ideal/Quotient/ChineseRemainder.lean

Statistics

Metric	Count
Definitions	0
Theorems `ker_tensorProductMk_quotient`, `pi_mkQ_rTensor`, `pi_tensorProductMk_quotient_surjective`	3
Total	3

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_tensorProductMk_quotient` 📖	mathematical	`Pairwise` `Function.onFun` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsCoprime` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring`	`LinearMap.ker` `AddCommGroup.toAddCommMonoid` `Pi.addCommMonoid` `TensorProduct` `HasQuotient.Quotient` `instHasQuotient_1` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `TensorProduct.addCommMonoid` `Pi.module` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.pi` `DFunLike.coe` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `LinearMap.instFunLike` `Quotient.one` `Submodule` `Submodule.instSMul` `IsScalarTower.left` `iInf` `Submodule.instInfSet` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Top.top` `Submodule.instTop`	—	`rTensor_exact` `LinearMap.exact_subtype_ker_map` `pi_mkQ_surjective` `TensorProduct.smulCommClass_left` `smulCommClass_self` `IsScalarTower.left` `RingHomCompTriple.ids` `RingHomInvPair.ids` `RingHomSurjective.ids` `LinearMap.comp.congr_simp` `pi_mkQ_rTensor` `LinearEquiv.symm_trans_self` `LinearEquiv.ker_comp` `le_antisymm` `Submodule.smul_le` `LinearMap.ker_pi` `Submodule.ker_mkQ` `TensorProduct.induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Submodule.smul_mem_smul` `Subtype.mem` `map_add` `SemilinearMapClass.toAddHomClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `LinearMap.exact_iff` `LinearEquiv.conj_exact_iff_exact`
`pi_mkQ_rTensor` 📖	mathematical	—	`LinearMap.rTensor` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Pi.addCommMonoid` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `Semiring.toModule` `CommSemiring.toSemiring` `Submodule.hasQuotient` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Pi.module` `Submodule.Quotient.module` `LinearMap.pi` `Submodule.mkQ` `LinearMap.comp` `TensorProduct` `Ideal` `instHasQuotient_1` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `LinearEquiv.symm` `TensorProduct.piLeft` `DFunLike.coe` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `LinearMap.instFunLike` `Quotient.one` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `TensorProduct.lid`	—	`TensorProduct.AlgebraTensorModule.curry_injective` `IsScalarTower.right` `TensorProduct.isScalarTower` `Pi.isScalarTower` `Quotient.isScalarTower` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self` `LinearMap.ext_ring` `IsScalarTower.to_smulCommClass` `LinearMap.ext` `instIsTwoSided_1` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_smul` `TensorProduct.piRight_symm_apply`
`pi_tensorProductMk_quotient_surjective` 📖	mathematical	`Pairwise` `Function.onFun` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsCoprime` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Pi.addCommMonoid` `TensorProduct` `HasQuotient.Quotient` `instHasQuotient_1` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Quotient.commRing` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `TensorProduct.addCommMonoid` `Pi.module` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.pi` `LinearMap.addCommMonoid` `LinearMap.module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Quotient.one`	—	`LinearMap.rTensor_surjective` `pi_mkQ_surjective` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct.smulCommClass_left` `smulCommClass_self` `pi_mkQ_rTensor`

---

← Back to Index