Duality

📁 Source: Mathlib/GroupTheory/FiniteAbelian/Duality.lean

Statistics

Metric	Count
Definitions	0
Theorems card_monoidHom_of_hasEnoughRootsOfUnity, exists_apply_ne_one_of_hasEnoughRootsOfUnity, monoidHom_mulEquiv_of_hasEnoughRootsOfUnity, restrict_surjective	4
Total	4

CommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_monoidHom_of_hasEnoughRootsOfUnity 📖	mathematical	—	Nat.card MonoidHom Units CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup Units.instMulOneClass	—	Nat.card_congr monoidHom_mulEquiv_of_hasEnoughRootsOfUnity
exists_apply_ne_one_of_hasEnoughRootsOfUnity 📖	—	—	—	—	Monoid.neZero_exponent_of_finite HasEnoughRootsOfUnity.of_dvd ZMod.exists_monoidHom_apply_ne_one HasEnoughRootsOfUnity.exists_primitiveRoot
monoidHom_mulEquiv_of_hasEnoughRootsOfUnity 📖	mathematical	—	MulEquiv MonoidHom Units CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup Units.instMulOneClass MonoidHom.mul toCommMonoid Units.instCommGroupUnits MulOne.toMul	—	equiv_prod_multiplicative_zmod_of_finite NeZero.of_gt Nat.instCanonicallyOrderedAdd Nat.card_eq_fintype_card Fintype.card_multiplicative ZMod.card Finite.of_fintype HasEnoughRootsOfUnity.of_dvd Monoid.neZero_exponent_of_finite IsCyclic.monoidHom_equiv_self instFiniteMultiplicative isCyclic_multiplicative ZMod.instIsAddCyclic

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrict_surjective 📖	mathematical	—	MonoidHom Units CommMonoid.toMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup CommGroup.toCommMonoid Units.instCommGroupUnits Subgroup SetLike.instMembership Subgroup.instSetLike SubmonoidClass.toMulOneClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass DFunLike.coe instCommMonoid instFunLike restrictHom	—	Subgroup.instFiniteSubtypeMem HasEnoughRootsOfUnity.of_dvd Monoid.neZero_exponent_of_finite Monoid.exponent_submonoid_dvd Subgroup.normal_of_comm Group.exponent_quotient_dvd surjective_of_card_ker_le_div SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass le_of_eq CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity Subgroup.card_eq_card_quotient_mul_card_subgroup mul_div_cancel_right₀ Nat.instMulDivCancelClass Fintype.card_ne_zero One.instNonempty Fintype.card_eq_nat_card Subgroup.finite_quotient_of_finiteIndex Subgroup.finiteIndex_of_finite Nat.card_congr

---

← Back to Index