Synonym

Statistics

Metric	Count
Definitions `instAddCommGroupWithOne`, `instAddCommMonoidWithOne`, `instAddGroupWithOne`, `instAddMonoidWithOne`, `instCommRing`, `instCommSemiring`, `instDistrib`, `instHasDistribNeg`, `instIntCast`, `instNatCast`, `instNonAssocRing`, `instNonAssocSemiring`, `instNonUnitalCommRing`, `instNonUnitalCommSemiring`, `instNonUnitalNonAssocRing`, `instNonUnitalNonAssocSemiring`, `instNonUnitalRing`, `instNonUnitalSemiring`, `instRing`, `instSemiring`, `instCommRingLex`, `instCommSemiringLex`, `instDistribLex`, `instHasDistribNegLex`, `instNonAssocRingLex`, `instNonAssocSemiringLex`, `instNonUnitalCommRingLex`, `instNonUnitalCommSemiringLex`, `instNonUnitalNonAssocRingLex`, `instNonUnitalNonAssocSemiringLex`, `instNonUnitalRingLex`, `instNonUnitalSemiringLex`, `instRingLex`, `instSemiringLex`	34
Theorems `instIsDomain`, `instLeftDistribClass`, `instRightDistribClass`, `instIsDomainLex`, `instLeftDistribClassLex`, `instRightDistribClassLex`, `ofDual_intCast`, `ofDual_natCast`, `ofDual_ofNat`, `toDual_intCast`, `toDual_natCast`, `toDual_ofNat`	12
Total	46

Name	Category	Theorems
`instAddCommGroupWithOne` 📖	CompOp	—
`instAddCommMonoidWithOne` 📖	CompOp	—
`instAddGroupWithOne` 📖	CompOp	—
`instAddMonoidWithOne` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instCommSemiring` 📖	CompOp	—
`instDistrib` 📖	CompOp	—
`instHasDistribNeg` 📖	CompOp	—
`instIntCast` 📖	CompOp	2 math math: `toDual_intCast`, `ofDual_intCast`
`instNatCast` 📖	CompOp	2 math math: `ofDual_natCast`, `toDual_natCast`
`instNonAssocRing` 📖	CompOp	—
`instNonAssocSemiring` 📖	CompOp	—
`instNonUnitalCommRing` 📖	CompOp	—
`instNonUnitalCommSemiring` 📖	CompOp	—
`instNonUnitalNonAssocRing` 📖	CompOp	—
`instNonUnitalNonAssocSemiring` 📖	CompOp	—
`instNonUnitalRing` 📖	CompOp	—
`instNonUnitalSemiring` 📖	CompOp	—
`instRing` 📖	CompOp	—
`instSemiring` 📖	CompOp	1 math math: `instIsDomain`

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDomain` 📖	mathematical	—	`IsDomain` `OrderDual` `instSemiring` `Ring.toSemiring`	—	`IsLeftCancelMulZero.mul_left_cancel_of_ne_zero` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `IsRightCancelMulZero.mul_right_cancel_of_ne_zero` `IsCancelMulZero.toIsRightCancelMulZero` `instNontrivial` `IsDomain.toNontrivial`
`instLeftDistribClass` 📖	mathematical	—	`LeftDistribClass` `OrderDual` `instMul` `instAdd`	—	—
`instRightDistribClass` 📖	mathematical	—	`RightDistribClass` `OrderDual` `instMul` `instAdd`	—	—

Name	Category	Theorems
`instCommRingLex` 📖	CompOp	—
`instCommSemiringLex` 📖	CompOp	—
`instDistribLex` 📖	CompOp	—
`instHasDistribNegLex` 📖	CompOp	—
`instNonAssocRingLex` 📖	CompOp	—
`instNonAssocSemiringLex` 📖	CompOp	—
`instNonUnitalCommRingLex` 📖	CompOp	—
`instNonUnitalCommSemiringLex` 📖	CompOp	—
`instNonUnitalNonAssocRingLex` 📖	CompOp	—
`instNonUnitalNonAssocSemiringLex` 📖	CompOp	—
`instNonUnitalRingLex` 📖	CompOp	—
`instNonUnitalSemiringLex` 📖	CompOp	—
`instRingLex` 📖	CompOp	—
`instSemiringLex` 📖	CompOp	3 math math: `HahnSeries.instIsStrictOrderedRingLexOfIsDomain`, `HahnSeries.instIsOrderedRingLexOfNoZeroDivisors`, `instIsDomainLex`

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsDomainLex` 📖	mathematical	—	`IsDomain` `Lex` `instSemiringLex` `Ring.toSemiring`	—	—
`instLeftDistribClassLex` 📖	mathematical	—	`LeftDistribClass` `Lex` `instMulLex` `instAddLex`	—	—
`instRightDistribClassLex` 📖	mathematical	—	`RightDistribClass` `Lex` `instMulLex` `instAddLex`	—	—
`ofDual_intCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderDual.instIntCast`	—	—
`ofDual_natCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderDual.instNatCast`	—	—
`ofDual_ofNat` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`toDual_intCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `OrderDual.instIntCast`	—	—
`toDual_natCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `OrderDual.instNatCast`	—	—
`toDual_ofNat` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—

---