Documentation Verification Report

Rat

📁 Source: Mathlib/Algebra/Star/Rat.lean

Statistics

Metric	Count
Definitions `instStarRing`, `instStarRing`	2
Theorems `instTrivialStar`, `instTrivialStar`, `star_nnratCast`, `star_ratCast`	4
Total	6

NNRat

Definitions

Name	Category	Theorems
`instStarRing` 📖	CompOp	3 math math: `StarAddMonoid.toStarModuleNNRat`, `instStarOrderedRing`, `instTrivialStar`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTrivialStar` 📖	mathematical	—	`TrivialStar` `NNRat` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield` `StarRing.toStarAddMonoid` `instStarRing`	—	—

Rat

Definitions

Name	Category	Theorems
`instStarRing` 📖	CompOp	3 math math: `StarAddMonoid.toStarModuleRat`, `instTrivialStar`, `instStarOrderedRing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTrivialStar` 📖	mathematical	—	`TrivialStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `StarRing.toStarAddMonoid` `instStarRing`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`star_nnratCast` 📖	mathematical	—	`Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `StarRing.toStarAddMonoid` `NNRat.cast` `DivisionSemiring.toNNRatCast`	—	`map_nnratCast` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `MulOpposite.unop_nnratCast`
`star_ratCast` 📖	mathematical	—	`Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `StarRing.toStarAddMonoid` `DivisionRing.toRatCast`	—	`map_ratCast` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `MulOpposite.unop_ratCast`

---

← Back to Index