Basic

📁 Source: Mathlib/RingTheory/RootsOfUnity/Basic.lean

Statistics

Metric	Count
Definitions monoidHomMulEquivRootsOfUnityOfGenerator, restrictRootsOfUnity, restrictRootsOfUnity, rootsOfUnity, fintype, mkOfPowEq, rootsOfUnityEquivNthRoots, rootsOfUnityUnitsMulEquiv	8
Theorems monoidHom_mulEquiv_rootsOfUnity, restrictRootsOfUnity_coe_apply, restrictRootsOfUnity_symm, val_set_image_rootsOfUnity, val_set_image_rootsOfUnity_one, val_set_image_rootsOfUnity_two, card_rootsOfUnity, disjoint_rootsOfUnity_of_coprime, instFiniteMonoidHomUnits, instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat, ker_zpowGroupHom_eq_rootsOfUnity, map_rootsOfUnity, map_rootsOfUnity_eq_pow_self, mem_rootsOfUnity, mem_rootsOfUnity', mem_rootsOfUnity_iff_mem_nthRoots, mem_rootsOfUnity_prime_pow_mul_iff, mem_rootsOfUnity_prime_pow_mul_iff', restrictRootsOfUnity_coe_apply, coe_injective, coe_mkOfPowEq, coe_pow, isCyclic, val_mkOfPowEq_coe, rootsOfUnityEquivNthRoots_apply, rootsOfUnityEquivNthRoots_symm_apply, rootsOfUnity_eq_ker, rootsOfUnity_inf_rootsOfUnity, rootsOfUnity_le_of_dvd, rootsOfUnity_one, rootsOfUnity_zero	31
Total	39

IsCyclic

Definitions

Name	Category	Theorems
monoidHomMulEquivRootsOfUnityOfGenerator 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monoidHom_mulEquiv_rootsOfUnity 📖	mathematical	—	MulEquiv MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Units CommMonoid.toMonoid CommGroup.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Nat.card MonoidHom.mul Subgroup.mul	—	exists_generator

MulEquiv

Definitions

Name	Category	Theorems
restrictRootsOfUnity 📖	CompOp	2 math math: restrictRootsOfUnity_symm, restrictRootsOfUnity_coe_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
restrictRootsOfUnity_coe_apply 📖	mathematical	—	Units.val CommMonoid.toMonoid Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike instEquivLike restrictRootsOfUnity MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
restrictRootsOfUnity_symm 📖	mathematical	—	symm Units CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Subgroup.mul restrictRootsOfUnity MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_set_image_rootsOfUnity 📖	mathematical	—	Set.image Units CommMonoid.toMonoid val SetLike.coe Subgroup instGroup Subgroup.instSetLike rootsOfUnity setOf Monoid.toNatPow MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	Set.ext mem_rootsOfUnity' Subtype.coe_prop
val_set_image_rootsOfUnity_one 📖	mathematical	—	Set.image Units CommMonoid.toMonoid val SetLike.coe Subgroup instGroup Subgroup.instSetLike rootsOfUnity Set Set.instSingletonSet MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	rootsOfUnity_one Set.image_singleton
val_set_image_rootsOfUnity_two 📖	mathematical	—	Set.image Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring val SetLike.coe Subgroup CommMonoid.toMonoid CommRing.toCommMonoid instGroup Subgroup.instSetLike rootsOfUnity Set Set.instInsert AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Set.instSingletonSet NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Set.ext val_set_image_rootsOfUnity

(root)

Definitions

Name	Category	Theorems
restrictRootsOfUnity 📖	CompOp	1 math math: restrictRootsOfUnity_coe_apply
rootsOfUnity 📖	CompOp	85 math math: mem_rootsOfUnity, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, modularCyclotomicCharacter.id, rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val, autAdjoinRootXPowSubCEquiv_root, ZMod.rootsOfUnity_eq_top, cyclotomicCharacter.toZModPow, ker_zpowGroupHom_eq_rootsOfUnity, IsPrimitiveRoot.val_toRootsOfUnity_coe, rootsOfUnity.integer_power_of_ringEquiv, rootsOfUnity.isCyclic, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, autAdjoinRootXPowSubCEquiv_symm_smul, IsCyclic.monoidHom_mulEquiv_rootsOfUnity, mem_rootsOfUnity_prime_pow_mul_iff', SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, Complex.mem_rootsOfUnity, Ideal.rootsOfUnityMapQuot_injective, mem_rootsOfUnity_iff_mem_nthRoots, rootsOfUnity.coe_injective, disjoint_rootsOfUnity_of_coprime, rootsOfUnity_one, HasEnoughRootsOfUnity.natCard_rootsOfUnity, rootsOfUnity.val_mkOfPowEq_coe, NumberField.Units.map_complexEmbedding_torsion, MulEquiv.restrictRootsOfUnity_symm, IsPrimitiveRoot.coe_autToPow_apply, HasEnoughRootsOfUnity.rootsOfUnity_isCyclic, IsPrimitiveRoot.card_rootsOfUnity', Units.val_set_image_rootsOfUnity_one, modularCyclotomicCharacter.toFun_spec, MulChar.apply_mem_rootsOfUnity_of_pow_eq_one, MulEquiv.restrictRootsOfUnity_coe_apply, IsPrimitiveRoot.card_rootsOfUnity, HasEnoughRootsOfUnity.cyc, Units.val_set_image_rootsOfUnity, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, map_rootsOfUnity_eq_pow_self, rootsOfUnity_eq_ker, AddChar.val_mem_rootsOfUnity, bijective_rootsOfUnityAddChar, rootsOfUnity.coe_mkOfPowEq, surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar, rootsOfUnity_inf_rootsOfUnity, SpecialLinearGroup.centerEquivRootsOfUnity_apply, NumberField.Units.rootsOfUnity_eq_torsion, Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, Units.val_set_image_rootsOfUnity_two, cyclotomicCharacter.toZModPow_toFun, IsPrimitiveRoot.zpowers_eq, modularCyclotomicCharacter.comp, rootsOfUnity_le_of_dvd, rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, rootsOfUnityEquivNthRoots_apply, card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot, rootsOfUnityCircleEquiv_apply, Complex.card_rootsOfUnity, IsPrimitiveRoot.mem_rootsOfUnity, NumberField.Units.rootsOfUnity_eq_one, autEquivRootsOfUnity_apply_rootOfSplit, SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply, rootsOfUnity.coe_pow, restrictRootsOfUnity_coe_apply, HasEnoughRootsOfUnity.finite_rootsOfUnity, IsPrimitiveRoot.val_inv_toRootsOfUnity_coe, mem_rootsOfUnity', card_rootsOfUnity, MulChar.apply_mem_rootsOfUnity_orderOf, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe, autAdjoinRootXPowSubC_root, rootsOfUnityEquivNthRoots_symm_apply, instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat, MulChar.apply_mem_rootsOfUnity, rootsOfUnityEquivOfPrimitiveRoots_symm_apply, map_rootsOfUnity, modularCyclotomicCharacter.aux_spec, ZMod.rootsOfUnityAddChar_val, rootsOfUnity_zero, modularCyclotomicCharacter.toFun_spec'', cyclotomicCharacter.toFun_spec, SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one, mem_rootsOfUnity_prime_pow_mul_iff, IsPrimitiveRoot.map_rootsOfUnity, rootsOfUnity.eq_one, autEquivRootsOfUnity_smul
rootsOfUnityEquivNthRoots 📖	CompOp	2 math math: rootsOfUnityEquivNthRoots_apply, rootsOfUnityEquivNthRoots_symm_apply
rootsOfUnityUnitsMulEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_rootsOfUnity 📖	mathematical	—	Fintype.card Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype	—	Fintype.card_congr Multiset.card_le_card Multiset.dedup_le Multiset.card_attach Polynomial.card_nthRoots
disjoint_rootsOfUnity_of_coprime 📖	mathematical	—	Disjoint Subgroup Units CommMonoid.toMonoid Units.instGroup Subgroup.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Subgroup.instCompleteLattice rootsOfUnity	—	rootsOfUnity_inf_rootsOfUnity rootsOfUnity_one
instFiniteMonoidHomUnits 📖	mathematical	—	Finite MonoidHom Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne Monoid.toMulOneClass LeftCancelMonoid.toMonoid Units.instMulOneClass	—	Finite.of_injective Pi.finite Finite.of_fintype Monoid.neZero_exponent_of_finite DFunLike.coe_injective Finite.of_surjective mem_rootsOfUnity map_pow MonoidHom.instMonoidHomClass Monoid.pow_exponent_eq_one map_one MonoidHomClass.toOneHomClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass MonoidHom.ext
instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat 📖	mathematical	—	Units CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity	—	rootsOfUnity_one
ker_zpowGroupHom_eq_rootsOfUnity 📖	mathematical	—	MonoidHom.ker Units CommMonoid.toMonoid Units.instGroup Units.instMulOneClass zpowGroupHom CommGroup.toDivisionCommMonoid Units.instCommGroupUnits rootsOfUnity	—	Subgroup.ext
map_rootsOfUnity 📖	mathematical	—	Subgroup Units CommMonoid.toMonoid Units.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.map rootsOfUnity	—	MonoidHom.instMonoidHomClass map_one MonoidHomClass.toOneHomClass
map_rootsOfUnity_eq_pow_self 📖	mathematical	—	DFunLike.coe Units.val CommMonoid.toMonoid CommRing.toCommMonoid Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	MonoidHom.map_cyclic rootsOfUnity.isCyclic restrictRootsOfUnity_coe_apply zpow_mod_orderOf pos_iff_ne_zero Nat.instCanonicallyOrderedAdd orderOf_pos Finite.of_fintype zpow_natCast rootsOfUnity.coe_pow
mem_rootsOfUnity 📖	mathematical	—	Units CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Monoid.toNatPow Units.instMonoid Units.instOne	—	—
mem_rootsOfUnity' 📖	mathematical	—	Units CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Monoid.toNatPow Units.val MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	mem_rootsOfUnity
mem_rootsOfUnity_iff_mem_nthRoots 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Subgroup CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Multiset Multiset.instMembership Polynomial.nthRoots AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Units.val	—	Polynomial.mem_nthRoots NeZero.pos Nat.instCanonicallyOrderedAdd
mem_rootsOfUnity_prime_pow_mul_iff 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Subgroup CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Monoid.toNatPow Nat.instMonoid	—	—
mem_rootsOfUnity_prime_pow_mul_iff' 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow Units.instMonoid Nat.instMonoid Units.instOne Subgroup CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity	—	mem_rootsOfUnity mem_rootsOfUnity_prime_pow_mul_iff
restrictRootsOfUnity_coe_apply 📖	mathematical	—	Units.val CommMonoid.toMonoid Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.instFunLike restrictRootsOfUnity	—	—
rootsOfUnityEquivNthRoots_apply 📖	mathematical	—	Multiset Multiset.instMembership Polynomial.nthRoots AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe Equiv Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity EquivLike.toFunLike Equiv.instEquivLike rootsOfUnityEquivNthRoots Units.val	—	—
rootsOfUnityEquivNthRoots_symm_apply 📖	mathematical	—	Units.val CommMonoid.toMonoid CommRing.toCommMonoid Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity DFunLike.coe Equiv Multiset Multiset.instMembership Polynomial.nthRoots AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing EquivLike.toFunLike Equiv.instEquivLike Equiv.symm rootsOfUnityEquivNthRoots	—	—
rootsOfUnity_eq_ker 📖	mathematical	—	rootsOfUnity MonoidHom.ker Units CommMonoid.toMonoid Units.instGroup Units.instMulOneClass powMonoidHom CommGroup.toCommMonoid Units.instCommGroupUnits	—	—
rootsOfUnity_inf_rootsOfUnity 📖	mathematical	—	Subgroup Units CommMonoid.toMonoid Units.instGroup Subgroup.instMin rootsOfUnity	—	Subgroup.ext
rootsOfUnity_le_of_dvd 📖	mathematical	—	Subgroup Units CommMonoid.toMonoid Units.instGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder rootsOfUnity	—	pow_mul one_pow
rootsOfUnity_one 📖	mathematical	—	rootsOfUnity Bot.bot Subgroup Units CommMonoid.toMonoid Units.instGroup Subgroup.instBot	—	Subgroup.ext pow_one
rootsOfUnity_zero 📖	mathematical	—	rootsOfUnity Top.top Subgroup Units CommMonoid.toMonoid Units.instGroup Subgroup.instTop	—	Subgroup.ext pow_zero

rootsOfUnity

Definitions

Name	Category	Theorems
fintype 📖	CompOp	13 math math: modularCyclotomicCharacter.id, cyclotomicCharacter.toZModPow, modularCyclotomicCharacter.toFun_spec', IsPrimitiveRoot.card_rootsOfUnity', modularCyclotomicCharacter.toFun_spec, IsPrimitiveRoot.card_rootsOfUnity, cyclotomicCharacter.toZModPow_toFun, modularCyclotomicCharacter.comp, card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot, Complex.card_rootsOfUnity, modularCyclotomicCharacter'.spec', card_rootsOfUnity, modularCyclotomicCharacter.toFun_spec''
mkOfPowEq 📖	CompOp	3 math math: Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, val_mkOfPowEq_coe, coe_mkOfPowEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_injective 📖	mathematical	—	Units CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Units.val	—	Units.val_injective Subtype.val_injective
coe_mkOfPowEq 📖	mathematical	Monoid.toNatPow CommMonoid.toMonoid MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Units.val Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity mkOfPowEq	—	—
coe_pow 📖	mathematical	—	Units.val CommMonoid.toMonoid Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Subgroup.npow Monoid.toNatPow	—	Subgroup.coe_pow Units.val_pow_eq_pow_val
isCyclic 📖	mathematical	—	IsCyclic Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Subgroup.zpow	—	isCyclic_of_subgroup_isDomain Finite.of_fintype coe_injective
val_mkOfPowEq_coe 📖	mathematical	Monoid.toNatPow CommMonoid.toMonoid MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	Units.val Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity mkOfPowEq	—	—

---

← Back to Index