Documentation Verification Report

Ring

📁 Source: Mathlib/Algebra/Colimit/Ring.lean

Statistics

Metric	Count
Definitions `inv`, `map`, `of`, `ringEquiv`, `instAddCommMonoidDirectLimit`, `instCommRingDirectLimit`, `instDirectLimit`, `instInhabitedDirectLimit`, `instOneDirectLimit`, `instZeroDirectLimit`	10
Theorems `exists_inv`, `inv_mul_cancel`, `mul_inv_cancel`, `nontrivial`, `exists_of`, `congr_apply_of`, `congr_symm_apply_of`, `exists_of`, `hom_ext`, `hom_ext_iff`, `induction_on`, `lift_comp_of`, `lift_injective`, `lift_of`, `lift_of'`, `map_apply_of`, `map_comp`, `map_id`, `zero_exact`, `of_f`, `of_injective`, `quotientMk_of`, `ringEquiv_of`, `ringEquiv_symm_mk`	24
Total	34

Field.DirectLimit

Definitions

Name	Category	Theorems
`inv` 📖	CompOp	2 math math: `mul_inv_cancel`, `inv_mul_cancel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_inv` 📖	mathematical	—	`Ring.DirectLimit` `Field.toCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.instCommRingDirectLimit` `Ring.instOneDirectLimit`	—	`Ring.DirectLimit.induction_on` `RingHom.map_mul` `mul_inv_cancel₀` `RingHom.map_zero` `RingHom.map_one`
`inv_mul_cancel` 📖	mathematical	—	`Ring.DirectLimit` `Field.toCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.instCommRingDirectLimit` `inv` `Ring.instOneDirectLimit`	—	`mul_comm` `mul_inv_cancel`
`mul_inv_cancel` 📖	mathematical	—	`Ring.DirectLimit` `Field.toCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.instCommRingDirectLimit` `inv` `Ring.instOneDirectLimit`	—	`exists_inv` `inv.eq_1`
`nontrivial` 📖	mathematical	—	`Nontrivial` `Ring.DirectLimit` `Field.toCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike`	—	`RingHom.map_one` `Ring.DirectLimit.of.zero_exact` `one_ne_zero` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`

Ring

Definitions

Name	Category	Theorems
`instAddCommMonoidDirectLimit` 📖	CompOp	—
`instCommRingDirectLimit` 📖	CompOp	20 math math: `DirectLimit.congr_symm_apply_of`, `Field.DirectLimit.exists_inv`, `DirectLimit.congr_apply_of`, `DirectLimit.of_injective`, `Field.DirectLimit.mul_inv_cancel`, `DirectLimit.hom_ext_iff`, `DirectLimit.ringEquiv_of`, `DirectLimit.quotientMk_of`, `DirectLimit.map_id`, `DirectLimit.map_comp`, `DirectLimit.lift_comp_of`, `DirectLimit.ringEquiv_symm_mk`, `Field.DirectLimit.inv_mul_cancel`, `DirectLimit.lift_of`, `DirectLimit.exists_of`, `DirectLimit.Polynomial.exists_of`, `DirectLimit.lift_injective`, `DirectLimit.map_apply_of`, `DirectLimit.of_f`, `DirectLimit.lift_of'`
`instDirectLimit` 📖	CompOp	—
`instInhabitedDirectLimit` 📖	CompOp	—
`instOneDirectLimit` 📖	CompOp	3 math math: `Field.DirectLimit.exists_inv`, `Field.DirectLimit.mul_inv_cancel`, `Field.DirectLimit.inv_mul_cancel`
`instZeroDirectLimit` 📖	CompOp	—

Ring.DirectLimit

Definitions

Name	Category	Theorems
`map` 📖	CompOp	3 math math: `map_id`, `map_comp`, `map_apply_of`
`of` 📖	CompOp	14 math math: `congr_symm_apply_of`, `congr_apply_of`, `of_injective`, `hom_ext_iff`, `ringEquiv_of`, `quotientMk_of`, `lift_comp_of`, `ringEquiv_symm_mk`, `lift_of`, `exists_of`, `Polynomial.exists_of`, `map_apply_of`, `of_f`, `lift_of'`
`ringEquiv` 📖	CompOp	2 math math: `ringEquiv_of`, `ringEquiv_symm_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_apply_of` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingEquiv.toRingHom` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	`DFunLike.coe` `RingEquiv` `Ring.DirectLimit` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.instCommRingDirectLimit` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `congr` `of`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_apply_of`
`congr_symm_apply_of` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingEquiv.toRingHom` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	`DFunLike.coe` `RingEquiv` `Ring.DirectLimit` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.instCommRingDirectLimit` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `congr` `of`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_apply_of`
`exists_of` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Ring.DirectLimit` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.instCommRingDirectLimit` `RingHom.instFunLike` `of`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `FreeCommRing.induction_on` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `exists_ge_ge` `map_add` `AddMonoidHomClass.toAddHomClass` `of_f` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`hom_ext` 📖	—	`RingHom.comp` `Ring.DirectLimit` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.instCommRingDirectLimit` `of`	—	—	`Ideal.Quotient.ringHom_ext` `Ideal.instIsTwoSided_1` `FreeCommRing.hom_ext`
`hom_ext_iff` 📖	mathematical	—	`RingHom.comp` `Ring.DirectLimit` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.instCommRingDirectLimit` `of`	—	`hom_ext`
`induction_on` 📖	—	`DFunLike.coe` `RingHom` `Ring.DirectLimit` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.instCommRingDirectLimit` `RingHom.instFunLike` `of`	—	—	`exists_of`
`lift_comp_of` 📖	mathematical	—	`lift` `RingHom.comp` `Ring.DirectLimit` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.instCommRingDirectLimit` `of`	—	`hom_ext` `RingHom.ext` `lift_of`
`lift_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`Ring.DirectLimit` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.instCommRingDirectLimit` `RingHom.instFunLike` `lift`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `induction_on` `lift_of` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`lift_of` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`DFunLike.coe` `RingHom` `Ring.DirectLimit` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.instCommRingDirectLimit` `RingHom.instFunLike` `lift` `of`	—	`FreeCommRing.lift_of`
`lift_of'` 📖	mathematical	—	`lift` `Ring.DirectLimit` `Ring.instCommRingDirectLimit` `of` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`hom_ext` `RingHom.ext` `lift_of` `RingHomCompTriple.comp_eq` `RingHomCompTriple.right_ids`
`map_apply_of` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`DFunLike.coe` `RingHom` `Ring.DirectLimit` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ring.instCommRingDirectLimit` `map` `of`	—	`lift_of`
`map_comp` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`RingHom.comp` `Ring.DirectLimit` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ring.instCommRingDirectLimit` `map`	—	`hom_ext` `RingHom.ext` `map_apply_of`
`map_id` 📖	mathematical	—	`map` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom` `RingHom.comp` `Ring.DirectLimit` `DFunLike.coe` `RingHom.instFunLike` `Ring.instCommRingDirectLimit`	—	`hom_ext` `RingHom.ext` `map_apply_of` `RingHomCompTriple.comp_eq` `RingHomCompTriple.right_ids`
`of_f` 📖	mathematical	`Preorder.toLE`	`DFunLike.coe` `RingHom` `Ring.DirectLimit` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.instCommRingDirectLimit` `RingHom.instFunLike` `of`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.eq` `Submodule.subset_span`
`of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`Ring.DirectLimit` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ring.instCommRingDirectLimit` `of`	—	`NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `Equiv.comp_injective` `DirectLimit.mk_injective`
`quotientMk_of` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeCommRing` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `instCommRingFreeCommRing` `Ideal.instHasQuotient` `Ideal.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `setOf` `Preorder.toLE` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `FreeCommRing.of` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `Ring.DirectLimit` `Ring.instCommRingDirectLimit` `of`	—	`Ideal.instIsTwoSided_1`
`ringEquiv_of` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Ring.DirectLimit` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `DirectLimit` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.instCommRingDirectLimit` `DirectLimit.instMul` `Distrib.toAdd` `DirectLimit.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `ringEquiv` `of` `DirectLimit.setoid`	—	`NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `lift_of`
`ringEquiv_symm_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `DirectLimit` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ring.DirectLimit` `DirectLimit.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ring.instCommRingDirectLimit` `DirectLimit.instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `ringEquiv` `DirectLimit.setoid` `of`	—	`NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass`

Ring.DirectLimit.Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_of` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.map` `Ring.DirectLimit` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Ring.instCommRingDirectLimit` `Ring.DirectLimit.of`	—	`Polynomial.induction_on` `Ring.DirectLimit.exists_of` `Polynomial.map_C` `exists_ge_ge` `Polynomial.map_add` `Polynomial.map_map` `RingHom.ext` `Ring.DirectLimit.of_f` `Polynomial.map_mul` `Polynomial.map_pow` `Polynomial.map_X`

Ring.DirectLimit.of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zero_exact` 📖	mathematical	`DFunLike.coe` `RingHom` `Ring.DirectLimit` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ring.instCommRingDirectLimit` `Ring.DirectLimit.of` `Ring.instZeroDirectLimit`	`Preorder.toLE` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`DirectLimit.exists_eq_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `Ring.DirectLimit.ringEquiv_of` `map_zero` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`

---

← Back to Index