Documentation Verification Report

CompTypeclasses

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

Statistics

Metric	Count
Definitions `RingHomCompTriple`, `RingHomId`, `RingHomInvPair`, `RingHomSurjective`	4
Theorems `surjective`, `comp_apply`, `comp_eq`, `ids`, `right_ids`, `eq_id`, `comp_apply_eq`, `comp_apply_eq₂`, `comp_eq`, `comp_eq₂`, `ids`, `of_ringEquiv`, `triples`, `triples₂`, `comp`, `ids`, `instToRingHomRingEquiv`, `invPair`, `is_surjective`, `instRingHomIdId`	20
Total	24

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjective` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instFunLike`	—	`RingHomSurjective.is_surjective`

RingHomCompTriple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`RingHom.congr_fun` `comp_eq`
`comp_eq` 📖	mathematical	—	`RingHom.comp` `Semiring.toNonAssocSemiring`	—	—
`ids` 📖	mathematical	—	`RingHomCompTriple` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`RingHom.comp_id`
`right_ids` 📖	mathematical	—	`RingHomCompTriple` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`RingHom.id_comp`

RingHomId

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_id` 📖	mathematical	—	`RingHom.id` `Semiring.toNonAssocSemiring`	—	—

RingHomInvPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_apply_eq` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`RingHom.comp_apply` `comp_eq`
`comp_apply_eq₂` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`RingHom.comp_apply` `comp_eq₂`
`comp_eq` 📖	mathematical	—	`RingHom.comp` `Semiring.toNonAssocSemiring` `RingHom.id`	—	—
`comp_eq₂` 📖	mathematical	—	`RingHom.comp` `Semiring.toNonAssocSemiring` `RingHom.id`	—	—
`ids` 📖	mathematical	—	`RingHomInvPair` `RingHom.id` `Semiring.toNonAssocSemiring`	—	—
`of_ringEquiv` 📖	mathematical	—	`RingHomInvPair` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.symm`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.symm_toRingHom_comp_toRingHom`
`triples` 📖	mathematical	—	`RingHomCompTriple` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`comp_eq`
`triples₂` 📖	mathematical	—	`RingHomCompTriple` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`comp_eq₂`

RingHomSurjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`RingHomSurjective`	—	`RingHom.surjective` `RingHomCompTriple.comp_eq` `RingHom.coe_comp`
`ids` 📖	mathematical	—	`RingHomSurjective` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`is_surjective` `invPair` `RingHomInvPair.ids`
`instToRingHomRingEquiv` 📖	mathematical	—	`RingHomSurjective` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.surjective`
`invPair` 📖	mathematical	—	`RingHomSurjective`	—	`RingHomInvPair.comp_apply_eq₂`
`is_surjective` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	—

(root)

Definitions

Name	Category	Theorems
`RingHomCompTriple` 📖	CompData	5 math math: `RingHomInvPair.triples`, `RingHomInvPair.triples₂`, `RingHomCompTriple.right_ids`, `AlgHom.instRingHomCompTripleComp`, `RingHomCompTriple.ids`
`RingHomId` 📖	CompData	1 math math: `instRingHomIdId`
`RingHomInvPair` 📖	CompData	6 math math: `RingHomInvPair.instStarRingEnd`, `RingHomInvPair.symm`, `WittVector.inv_pair₂`, `WittVector.inv_pair₁`, `RingHomInvPair.ids`, `RingHomInvPair.of_ringEquiv`
`RingHomSurjective` 📖	CompData	8 math math: `RingHomSurjective.ids`, `RingHomSurjective.instToRingHomRingEquiv`, `RingHomSurjective.invPair`, `RingHom.instRingHomSurjectiveProdSnd`, `RingHomSurjective.comp`, `instRingHomSurjectiveForallEvalRingHom`, `RingHom.instRingHomSurjectiveProdFst`, `Ideal.Quotient.instRingHomSurjectiveQuotientMk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instRingHomIdId` 📖	mathematical	—	`RingHomId` `RingHom.id` `Semiring.toNonAssocSemiring`	—	—

---

← Back to Index