Units

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`index_posSubgroup` 📖	mathematical	—	`Subgroup.index` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `instGroup` `posSubgroup`	—	`Subgroup.index_eq_two_iff` `lt_or_gt_of_ne` `ne_zero` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `mul_neg` `mul_one` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `xor_true` `LT.lt.le` `xor_comm`

---