Synonym

Statistics

Metric	Count
Definitions `instCommRingLex`, `instCommRingOrderDual`, `instCommSemiringLex`, `instCommSemiringOrderDual`, `instDistribLex`, `instDistribOrderDual`, `instHasDistribNegLex`, `instHasDistribNegOrderDual`, `instNonAssocRingLex`, `instNonAssocRingOrderDual`, `instNonAssocSemiringLex`, `instNonAssocSemiringOrderDual`, `instNonUnitalCommRingLex`, `instNonUnitalCommRingOrderDual`, `instNonUnitalCommSemiringLex`, `instNonUnitalCommSemiringOrderDual`, `instNonUnitalNonAssocRingLex`, `instNonUnitalNonAssocRingOrderDual`, `instNonUnitalNonAssocSemiringLex`, `instNonUnitalNonAssocSemiringOrderDual`, `instNonUnitalRingLex`, `instNonUnitalRingOrderDual`, `instNonUnitalSemiringLex`, `instNonUnitalSemiringOrderDual`, `instRingLex`, `instRingOrderDual`, `instSemiringLex`, `instSemiringOrderDual`	28
Theorems `instIsDomainLex`, `instIsDomainOrderDual`, `instLeftDistribClassLex`, `instLeftDistribClassOrderDual`, `instRightDistribClassLex`, `instRightDistribClassOrderDual`	6
Total	34

Name	Category	Theorems
`instCommRingLex` 📖	CompOp	—
`instCommRingOrderDual` 📖	CompOp	—
`instCommSemiringLex` 📖	CompOp	—
`instCommSemiringOrderDual` 📖	CompOp	—
`instDistribLex` 📖	CompOp	—
`instDistribOrderDual` 📖	CompOp	—
`instHasDistribNegLex` 📖	CompOp	—
`instHasDistribNegOrderDual` 📖	CompOp	—
`instNonAssocRingLex` 📖	CompOp	—
`instNonAssocRingOrderDual` 📖	CompOp	—
`instNonAssocSemiringLex` 📖	CompOp	—
`instNonAssocSemiringOrderDual` 📖	CompOp	—
`instNonUnitalCommRingLex` 📖	CompOp	—
`instNonUnitalCommRingOrderDual` 📖	CompOp	—
`instNonUnitalCommSemiringLex` 📖	CompOp	—
`instNonUnitalCommSemiringOrderDual` 📖	CompOp	—
`instNonUnitalNonAssocRingLex` 📖	CompOp	—
`instNonUnitalNonAssocRingOrderDual` 📖	CompOp	—
`instNonUnitalNonAssocSemiringLex` 📖	CompOp	—
`instNonUnitalNonAssocSemiringOrderDual` 📖	CompOp	—
`instNonUnitalRingLex` 📖	CompOp	—
`instNonUnitalRingOrderDual` 📖	CompOp	—
`instNonUnitalSemiringLex` 📖	CompOp	—
`instNonUnitalSemiringOrderDual` 📖	CompOp	—
`instRingLex` 📖	CompOp	—
`instRingOrderDual` 📖	CompOp	—
`instSemiringLex` 📖	CompOp	3 math math: `HahnSeries.instIsStrictOrderedRingLexOfIsDomain`, `HahnSeries.instIsOrderedRingLexOfNoZeroDivisors`, `instIsDomainLex`
`instSemiringOrderDual` 📖	CompOp	1 math math: `instIsDomainOrderDual`

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDomainLex` 📖	mathematical	—	`IsDomain` `Lex` `instSemiringLex` `Ring.toSemiring`	—	—
`instIsDomainOrderDual` 📖	mathematical	—	`IsDomain` `OrderDual` `instSemiringOrderDual` `Ring.toSemiring`	—	—
`instLeftDistribClassLex` 📖	mathematical	—	`LeftDistribClass` `Lex` `instMulLex` `instAddLex`	—	—
`instLeftDistribClassOrderDual` 📖	mathematical	—	`LeftDistribClass` `OrderDual` `instMulOrderDual` `instAddOrderDual`	—	—
`instRightDistribClassLex` 📖	mathematical	—	`RightDistribClass` `Lex` `instMulLex` `instAddLex`	—	—
`instRightDistribClassOrderDual` 📖	mathematical	—	`RightDistribClass` `OrderDual` `instMulOrderDual` `instAddOrderDual`	—	—

---