CyclotomicCharacter

📁 Source: Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean

Statistics

Metric	Count
Definitions cyclotomicCharacter, toFun, modularCyclotomicCharacter, modularCyclotomicCharacter', aux, toFun	6
Theorems autToPow_eq_modularCyclotomicCharacter, continuous, spec, toFun_apply, toFun_spec, toZModPow, toZModPow_toFun, spec', unique', aux_spec, comp, id, pow_dvd_aux_pow_sub_aux_pow, spec, toFun_spec, toFun_spec', toFun_spec'', toFun_unique, toFun_unique', unique, integer_power_of_ringEquiv, integer_power_of_ringEquiv'	22
Total	28

IsPrimitiveRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
autToPow_eq_modularCyclotomicCharacter 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	DFunLike.coe MonoidHom AlgEquiv CommRing.toCommSemiring CommSemiring.toSemiring Units ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero ZMod.commRing MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut Units.instMulOneClass MonoidHom.instFunLike autToPow RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd RingAut.instGroup modularCyclotomicCharacter card_rootsOfUnity RingEquivClass.toRingEquiv AlgEquiv.instEquivLike AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass	—	Units.ext card_rootsOfUnity AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass ZMod.val_injective ZMod.val_lt autToPow_spec ZMod.ringEquivCongr_val modularCyclotomicCharacter.toFun_spec''

(root)

Definitions

Name	Category	Theorems
cyclotomicCharacter 📖	CompOp	3 math math: cyclotomicCharacter.toZModPow, cyclotomicCharacter.spec, cyclotomicCharacter.continuous
modularCyclotomicCharacter 📖	CompOp	5 math math: cyclotomicCharacter.toZModPow, modularCyclotomicCharacter.spec, IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter, modularCyclotomicCharacter.unique, cyclotomicCharacter.toZModPow_toFun
modularCyclotomicCharacter' 📖	CompOp	2 math math: modularCyclotomicCharacter'.spec', modularCyclotomicCharacter'.unique'

cyclotomicCharacter

Definitions

Name	Category	Theorems
toFun 📖	CompOp	3 math math: toFun_apply, toZModPow_toFun, toFun_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous 📖	mathematical	—	Continuous AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Units PadicInt MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring PadicInt.instCommRing krullTopology Units.instTopologicalSpaceUnits UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing PadicInt.instNormedCommRing DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AlgEquiv.aut Units.instMulOneClass MonoidHom.instFunLike MonoidHom.comp RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toAdd RingAut.instGroup cyclotomicCharacter instIsDomain MulSemiringAction.toRingAut AlgEquiv.applyMulSemiringAction	—	instIsDomain Continuous.of_coeHom_comp IsTopologicalGroup.toContinuousInv instIsTopologicalGroupAlgEquiv continuous_of_continuousAt_one IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing MonoidHom.instMonoidHomClass ContinuousAt.eq_1 map_one MonoidHomClass.toOneHomClass Filter.HasBasis.tendsto_iff GroupFilterBasis.nhds_one_hasBasis Metric.nhds_basis_ball PadicInt.exists_pow_neg_lt lt_of_le_of_lt zpow_le_zpow_right₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero Nat.Prime.one_le Fact.out neg_le_neg Int.instIsOrderedAddMonoid Nat.mono_cast Int.instAddLeftMono Int.instZeroLEOneClass Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd IntermediateField.adjoin.finiteDimensional IsIntegral.tower_top AddCommGroup.intIsScalarTower IsPrimitiveRoot.isIntegral NeZero.of_gt' Nat.Prime.one_lt' AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass dist_eq_norm PadicInt.norm_le_pow_iff_mem_span_pow RingHom.instRingHomClass PadicInt.ker_toZModPow RingHom.mem_ker map_sub RingHomClass.toAddMonoidHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Fintype.card_eq_nat_card HasEnoughRootsOfUnity.natCard_rootsOfUnity rootsOfUnity.isCyclic toZModPow sub_eq_zero modularCyclotomicCharacter.unique IsPrimitiveRoot.isUnit IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity IsPrimitiveRoot.isUnit_unit ZMod.val_one'' LT.lt.ne' one_lt_pow₀ Nat.instZeroLEOneClass IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.Prime.one_lt pow_one pow_mem SubsemiringClass.toSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IntermediateField.mem_adjoin_simple_self continuous_const
spec 📖	mathematical	HasEnoughRootsOfUnity CommRing.toCommMonoid Monoid.toNatPow Nat.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike ZMod.val RingHom PadicInt ZMod Semiring.toNonAssocSemiring PadicInt.instCommRing ZMod.commRing RingHom.instFunLike PadicInt.toZModPow Units.val MonoidHom Units MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup Units.instMulOneClass MonoidHom.instFunLike cyclotomicCharacter	—	toFun_spec NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt'
toFun_apply 📖	mathematical	HasEnoughRootsOfUnity CommRing.toCommMonoid Monoid.toNatPow Nat.instMonoid	toFun PadicInt.ofIntSeq modularCyclotomicCharacter.aux NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow	—	HasEnoughRootsOfUnity.exists_primitiveRoot
toFun_spec 📖	mathematical	HasEnoughRootsOfUnity CommRing.toCommMonoid Monoid.toNatPow Nat.instMonoid	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val CommMonoid.toMonoid Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.val RingHom PadicInt ZMod Semiring.toNonAssocSemiring PadicInt.instCommRing ZMod.commRing RingHom.instFunLike PadicInt.toZModPow toFun	—	NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Fintype.card_eq_nat_card HasEnoughRootsOfUnity.natCard_rootsOfUnity toZModPow_toFun modularCyclotomicCharacter.spec
toZModPow 📖	mathematical	HasEnoughRootsOfUnity CommRing.toCommMonoid Monoid.toNatPow Nat.instMonoid	DFunLike.coe RingHom PadicInt ZMod Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring PadicInt.instCommRing ZMod.commRing RingHom.instFunLike PadicInt.toZModPow Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd Units MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup Units.instMulOneClass MonoidHom.instFunLike cyclotomicCharacter modularCyclotomicCharacter NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' Fintype.card CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype Nat.card Fintype.card_eq_nat_card HasEnoughRootsOfUnity.natCard_rootsOfUnity	—	toZModPow_toFun
toZModPow_toFun 📖	mathematical	HasEnoughRootsOfUnity CommRing.toCommMonoid Monoid.toNatPow Nat.instMonoid	DFunLike.coe RingHom PadicInt ZMod Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring PadicInt.instCommRing ZMod.commRing RingHom.instFunLike PadicInt.toZModPow toFun Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero MonoidHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd Units MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup Units.instMulOneClass MonoidHom.instFunLike modularCyclotomicCharacter NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt' Fintype.card CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype Nat.card Fintype.card_eq_nat_card HasEnoughRootsOfUnity.natCard_rootsOfUnity	—	NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Fintype.card_eq_nat_card HasEnoughRootsOfUnity.natCard_rootsOfUnity PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow toFun_apply PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub map_intCast RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass

modularCyclotomicCharacter

Definitions

Name	Category	Theorems
aux 📖	CompOp	3 math math: pow_dvd_aux_pow_sub_aux_pow, cyclotomicCharacter.toFun_apply, aux_spec
toFun 📖	CompOp	7 math math: id, toFun_unique', toFun_spec', toFun_spec, comp, toFun_unique, toFun_spec''

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aux_spec 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val CommMonoid.toMonoid CommRing.toCommMonoid Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity DivInvMonoid.toZPow Units.instDivInvMonoid aux	—	rootsOfUnity.integer_power_of_ringEquiv
comp 📖	mathematical	—	toFun RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup ZMod Fintype.card Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype ZMod.commRing	—	toFun_unique toFun_spec Subgroup.coe_pow mul_comm pow_mul SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Nat.cast_mul ZMod.natCast_val Fintype.instNeZeroNatCardOfNonempty One.instNonempty ZMod.cast_mul orderOf_dvd_card ZMod.charP
id 📖	mathematical	—	toFun RingEquiv.refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd ZMod Fintype.card Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing	—	toFun_unique Fin.size_positive' Fintype.instNeZeroNatCardOfNonempty One.instNonempty LE.le.lt_or_eq ZMod.val_one pow_one Fintype.card_le_one_iff_subsingleton Eq.ge one_pow
pow_dvd_aux_pow_sub_aux_pow 📖	mathematical	HasEnoughRootsOfUnity CommRing.toCommMonoid Monoid.toNatPow Nat.instMonoid	Int.instMonoid aux NeZero.of_gt' AddMonoid.toAddZeroClass Nat.instAddMonoid Nat.instPreorder Nat.instCanonicallyOrderedAdd Nat.instOne Nat.Prime.one_lt'	—	NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE HasEnoughRootsOfUnity.exists_primitiveRoot IsPrimitiveRoot.pow IsPrimitiveRoot.isUnit Units.ext IsPrimitiveRoot.mem_rootsOfUnity IsPrimitiveRoot.isUnit_unit aux_spec Nat.cast_pow mul_dvd_mul_iff_left IsCancelMulZero.toIsLeftCancelMulZero Int.instIsCancelMulZero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors Int.instNormMulClass Int.instNontrivial Nat.cast_mul mul_sub mul_comm IsPrimitiveRoot.zpow_eq_one_iff_dvd div_eq_mul_inv div_eq_one Units.ext_iff Units.val_pow_eq_pow_val map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
spec 📖	mathematical	Fintype.card Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val Monoid.toNatPow ZMod.val ZMod ZMod.commRing MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup Units.instMulOneClass MonoidHom.instFunLike modularCyclotomicCharacter	—	toFun_spec' ZMod.ringEquivCongr_val
toFun_spec 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val CommMonoid.toMonoid CommRing.toCommMonoid Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Monoid.toNatPow Units.instMonoid ZMod.val Fintype.card rootsOfUnity.fintype toFun	—	aux_spec zpow_natCast toFun.eq_1 ZMod.val_intCast Fintype.instNeZeroNatCardOfNonempty One.instNonempty Subgroup.coe_zpow Units.ext_iff SetCoe.ext_iff zpow_eq_zpow_emod pow_card_eq_one
toFun_spec' 📖	mathematical	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Subgroup CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val Monoid.toNatPow ZMod.val Fintype.card rootsOfUnity.fintype toFun	—	toFun_spec
toFun_spec'' 📖	mathematical	IsPrimitiveRoot CommRing.toCommMonoid	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.val Fintype.card Units CommMonoid.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype toFun	—	toFun_spec' SetLike.coe_mem
toFun_unique 📖	mathematical	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val CommMonoid.toMonoid CommRing.toCommMonoid Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity Monoid.toNatPow Units.instMonoid ZMod.val Fintype.card rootsOfUnity.fintype	toFun	—	IsCyclic.ext Finite.of_fintype rootsOfUnity.isCyclic Nat.card_eq_fintype_card toFun_spec SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass
toFun_unique' 📖	mathematical	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val CommMonoid.toMonoid CommRing.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.val Fintype.card Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype	toFun	—	toFun_unique
unique 📖	mathematical	Fintype.card Units CommMonoid.toMonoid CommRing.toCommMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.val	ZMod ZMod.commRing MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup Units.instMulOneClass MonoidHom.instFunLike modularCyclotomicCharacter	—	toFun_unique' ZMod.ringEquivCongr_val ZMod.ringEquivCongr_symm RingEquiv.apply_symm_apply

modularCyclotomicCharacter'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spec' 📖	mathematical	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Subgroup CommMonoid.toMonoid CommRing.toCommMonoid Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val Monoid.toNatPow ZMod.val Fintype.card rootsOfUnity.fintype ZMod ZMod.commRing MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup Units.instMulOneClass MonoidHom.instFunLike modularCyclotomicCharacter'	—	modularCyclotomicCharacter.toFun_spec'
unique' 📖	mathematical	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val CommMonoid.toMonoid CommRing.toCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.val Fintype.card Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity rootsOfUnity.fintype	ZMod ZMod.commRing MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid RingAut.instGroup Units.instMulOneClass MonoidHom.instFunLike modularCyclotomicCharacter'	—	modularCyclotomicCharacter.toFun_unique'

rootsOfUnity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integer_power_of_ringEquiv 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val CommMonoid.toMonoid CommRing.toCommMonoid Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike rootsOfUnity DivInvMonoid.toZPow Units.instDivInvMonoid	—	RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass MonoidHom.map_cyclic isCyclic Units.ext_iff SetCoe.ext_iff
integer_power_of_ringEquiv' 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Units.val CommMonoid.toMonoid CommRing.toCommMonoid Units DivInvMonoid.toZPow Units.instDivInvMonoid	—	integer_power_of_ringEquiv

---

← Back to Index