Documentation Verification Report

InjSurj

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

Statistics

Metric	Count
Definitions `instHasDistribNeg`, `addCommGroupWithOne`, `addCommMonoidWithOne`, `addGroupWithOne`, `addMonoidWithOne`, `commRing`, `commSemiring`, `distrib`, `hasDistribNeg`, `nonAssocRing`, `nonAssocSemiring`, `nonUnitalCommRing`, `nonUnitalCommSemiring`, `nonUnitalNonAssocCommRing`, `nonUnitalNonAssocCommSemiring`, `nonUnitalNonAssocRing`, `nonUnitalNonAssocSemiring`, `nonUnitalRing`, `nonUnitalSemiring`, `semiring`, `addCommGroupWithOne`, `addCommMonoidWithOne`, `addGroupWithOne`, `addMonoidWithOne`, `commRing`, `commSemiring`, `distrib`, `hasDistribNeg`, `nonAssocRing`, `nonAssocSemiring`, `nonUnitalCommRing`, `nonUnitalCommSemiring`, `nonUnitalNonAssocCommRing`, `nonUnitalNonAssocCommSemiring`, `nonUnitalNonAssocRing`, `nonUnitalNonAssocSemiring`, `nonUnitalRing`, `nonUnitalSemiring`, `semiring`	39
Theorems `leftDistribClass`, `rightDistribClass`, `leftDistribClass`, `rightDistribClass`	4
Total	43

AddOpposite

Definitions

Name	Category	Theorems
`instHasDistribNeg` 📖	CompOp	—

Function.Injective

Definitions

Name	Category	Theorems
`addCommGroupWithOne` 📖	CompOp	—
`addCommMonoidWithOne` 📖	CompOp	—
`addGroupWithOne` 📖	CompOp	—
`addMonoidWithOne` 📖	CompOp	—
`commRing` 📖	CompOp	—
`commSemiring` 📖	CompOp	—
`distrib` 📖	CompOp	—
`hasDistribNeg` 📖	CompOp	—
`nonAssocRing` 📖	CompOp	—
`nonAssocSemiring` 📖	CompOp	—
`nonUnitalCommRing` 📖	CompOp	—
`nonUnitalCommSemiring` 📖	CompOp	—
`nonUnitalNonAssocCommRing` 📖	CompOp	—
`nonUnitalNonAssocCommSemiring` 📖	CompOp	—
`nonUnitalNonAssocRing` 📖	CompOp	—
`nonUnitalNonAssocSemiring` 📖	CompOp	—
`nonUnitalRing` 📖	CompOp	—
`nonUnitalSemiring` 📖	CompOp	—
`semiring` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leftDistribClass` 📖	mathematical	—	`LeftDistribClass`	—	`left_distrib`
`rightDistribClass` 📖	mathematical	—	`RightDistribClass`	—	`right_distrib`

Function.Surjective

Definitions

Name	Category	Theorems
`addCommGroupWithOne` 📖	CompOp	—
`addCommMonoidWithOne` 📖	CompOp	—
`addGroupWithOne` 📖	CompOp	—
`addMonoidWithOne` 📖	CompOp	—
`commRing` 📖	CompOp	—
`commSemiring` 📖	CompOp	—
`distrib` 📖	CompOp	—
`hasDistribNeg` 📖	CompOp	—
`nonAssocRing` 📖	CompOp	—
`nonAssocSemiring` 📖	CompOp	—
`nonUnitalCommRing` 📖	CompOp	—
`nonUnitalCommSemiring` 📖	CompOp	—
`nonUnitalNonAssocCommRing` 📖	CompOp	—
`nonUnitalNonAssocCommSemiring` 📖	CompOp	—
`nonUnitalNonAssocRing` 📖	CompOp	—
`nonUnitalNonAssocSemiring` 📖	CompOp	—
`nonUnitalRing` 📖	CompOp	—
`nonUnitalSemiring` 📖	CompOp	—
`semiring` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leftDistribClass` 📖	mathematical	—	`LeftDistribClass`	—	`forall₃` `left_distrib`
`rightDistribClass` 📖	mathematical	—	`RightDistribClass`	—	`forall₃` `right_distrib`

---

← Back to Index