Torsion

Statistics

Metric	Count
Definitions	0
Theorems `instHasEnoughRootsOfUnityHSubNatOfNat`, `rootsOfUnity_eq_top`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasEnoughRootsOfUnityHSubNatOfNat` 📖	mathematical	—	`HasEnoughRootsOfUnity` `ZMod` `CommRing.toCommMonoid` `commRing`	—	`Nat.Prime.two_le` `Fact.out` `HasEnoughRootsOfUnity.of_card_le` `instIsDomain` `Nat.card_congr` `rootsOfUnity_eq_top` `Nat.card_eq_fintype_card` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Fintype.card_subtype_true` `Fintype.card_units` `card`
`rootsOfUnity_eq_top` 📖	mathematical	—	`rootsOfUnity` `ZMod` `CommRing.toCommMonoid` `commRing` `Top.top` `Subgroup` `Units` `CommMonoid.toMonoid` `Units.instGroup` `Subgroup.instTop`	—	`Subgroup.ext` `pow_card_sub_one_eq_one` `Units.ne_zero` `nontrivial` `Nat.Prime.one_lt'`

---