Duality

Statistics

Metric	Count
Definitions	0
Theorems `card_eq_card_units_of_hasEnoughRootsOfUnity`, `exists_apply_ne_one_iff_exists_monoidHom`, `exists_apply_ne_one_of_hasEnoughRootsOfUnity`, `finite`, `mulEquiv_units`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eq_card_units_of_hasEnoughRootsOfUnity` 📖	mathematical	—	`Nat.card` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Units` `CommMonoid.toMonoid`	—	`Nat.card_congr` `mulEquiv_units`
`exists_apply_ne_one_iff_exists_monoidHom` 📖	—	—	—	—	`Mathlib.Tactic.Contrapose.contrapose₄` `coe_toUnitHom` `Units.ext_iff` `equivToUnitHom_symm_coe`
`exists_apply_ne_one_of_hasEnoughRootsOfUnity` 📖	—	—	—	—	`exists_apply_ne_one_iff_exists_monoidHom` `CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity` `instFiniteUnits` `Mathlib.Tactic.Contrapose.contrapose₄` `IsUnit.unit_spec` `Units.val_eq_one` `map_nonunit` `zero_ne_one` `NeZero.one`
`finite` 📖	mathematical	—	`Finite` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring`	—	`Finite.of_equiv` `instFiniteMonoidHomUnits`
`mulEquiv_units` 📖	mathematical	—	`MulEquiv` `MulChar` `CommSemiring.toCommMonoidWithZero` `CommRing.toCommSemiring` `Units` `CommMonoid.toMonoid` `hasMul` `Units.instMul`	—	`CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity` `instFiniteUnits`

---