Units

Statistics

Metric	Count
Definitions	0
Theorems `units_eq_one_or`, `units_ne_iff_eq_neg`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`units_eq_one_or` 📖	mathematical	—	`Units` `instMonoid` `Units.instOne` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing`	—	`isUnit_eq_one_or` `Units.isUnit`
`units_ne_iff_eq_neg` 📖	mathematical	—	`Units` `instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing`	—	`isUnit_ne_iff_eq_neg` `Units.isUnit`

---