GrindInstances

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

Statistics

Metric	Count
Definitions toGrindCommRing, toGrindCommSemiring, toGrindRing, toGrindSemiring	4
Theorems toGrindSemiring_ofNat	1
Total	5

CommRing

Definitions

Name	Category	Theorems
toGrindCommRing 📖	CompOp	—

CommSemiring

Definitions

Name	Category	Theorems
toGrindCommSemiring 📖	CompOp	—

Ring

Definitions

Name	Category	Theorems
toGrindRing 📖	CompOp	—

Semiring

Definitions

Name	Category	Theorems
toGrindSemiring 📖	CompOp	3 math math: instIsCharPOfIsLeftCancelAddOfCharP, toGrindSemiring_ofNat, instOrderedRingOfIsStrictOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toGrindSemiring_ofNat 📖	mathematical	—	toGrindSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne toNonAssocSemiring	—	Nat.cast_zero Nat.cast_one

---

← Back to Index