Documentation Verification Report

Shrink

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

Statistics

Metric	Count
Definitions `instAddGroupWithOne`, `instAddMonoidWithOne`, `instCommRing`, `instCommSemiring`, `instNonAssocRing`, `instNonAssocSemiring`, `instNonUnitalCommRing`, `instNonUnitalCommSemiring`, `instNonUnitalNonAssocRing`, `instNonUnitalNonAssocSemiring`, `instNonUnitalRing`, `instNonUnitalSemiring`, `instRing`, `instSemiring`, `ringEquiv`	15
Theorems `instIsDomain`	1
Total	16

Shrink

Definitions

Name	Category	Theorems
`instAddGroupWithOne` 📖	CompOp	—
`instAddMonoidWithOne` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instCommSemiring` 📖	CompOp	—
`instNonAssocRing` 📖	CompOp	—
`instNonAssocSemiring` 📖	CompOp	—
`instNonUnitalCommRing` 📖	CompOp	—
`instNonUnitalCommSemiring` 📖	CompOp	—
`instNonUnitalNonAssocRing` 📖	CompOp	—
`instNonUnitalNonAssocSemiring` 📖	CompOp	—
`instNonUnitalRing` 📖	CompOp	—
`instNonUnitalSemiring` 📖	CompOp	—
`instRing` 📖	CompOp	—
`instSemiring` 📖	CompOp	3 math math: `algEquiv_apply`, `instIsDomain`, `algEquiv_symm_apply`
`ringEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDomain` 📖	mathematical	—	`IsDomain` `Shrink` `instSemiring`	—	`Equiv.isDomain`

---

← Back to Index