ZMod

📁 Source: Mathlib/Analysis/Fourier/ZMod.lean

Statistics

Metric	Count
Definitions dft, term𝓕, «term𝓕⁻»	3
Theorems fourierTransform_eq_inv_mul_gaussSum, fourierTransform_eq_gaussSum_mulShift, dft_apply, dft_apply_zero, dft_comp_neg, dft_comp_unitMul, dft_const_mul, dft_const_smul, dft_def, dft_dft, dft_eq_fourier, dft_even_iff, dft_mul_const, dft_odd_iff, dft_smul_const, invDFT_apply, invDFT_apply', invDFT_def, invDFT_def'	19
Total	22

DirichletCharacter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourierTransform_eq_gaussSum_mulShift 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Complex.addCommGroup Pi.Function.module Complex.instModuleSelf EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ZMod.dft DirichletCharacter CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing gaussSum ZMod.fintype Complex.commRing AddChar.mulShift CommRing.toRing ZMod.stdAddChar NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	RingHomInvPair.ids Finset.sum_congr AddChar.mulShift_apply mul_comm neg_mul ZMod.stdAddChar_apply

DirichletCharacter.IsPrimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fourierTransform_eq_inv_mul_gaussSum 📖	mathematical	DirichletCharacter.IsPrimitive Complex CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField	DFunLike.coe LinearEquiv Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Complex.addCommGroup Pi.Function.module Complex.instModuleSelf EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv ZMod.dft DirichletCharacter MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing Complex.instMul MulChar.hasInv NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing gaussSum ZMod.fintype Complex.commRing ZMod.stdAddChar	—	RingHomInvPair.ids DirichletCharacter.fourierTransform_eq_gaussSum_mulShift gaussSum_mulShift_of_isPrimitive instIsDomain

ZMod

Definitions

Name	Category	Theorems
dft 📖	CompOp	23 math math: LFunction_one_sub, dft_even_iff, invDFT_apply, dft_mul_const, dft_comp_unitMul, invDFT_def', dft_apply, invDFT_apply', dft_comp_neg, DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum, dft_dft, completedLFunction_one_sub_odd, dft_const_mul, invDFT_def, completedLFunction_one_sub_even, DirichletCharacter.fourierTransform_eq_gaussSum_mulShift, dft_eq_fourier, dft_odd_iff, LFunction_dft, dft_const_smul, dft_smul_const, dft_def, dft_apply_zero
term𝓕 📖	CompOp	—
«term𝓕⁻» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dft_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft Finset.sum Finset.univ fintype SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing commRing AddChar.instFunLike stdAddChar NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids
dft_apply_zero 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Finset.sum Finset.univ fintype	—	RingHomInvPair.ids Finset.sum_congr MulZeroClass.mul_zero neg_zero AddChar.map_zero_eq_one one_smul
dft_comp_neg 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing	—	—
dft_comp_unitMul 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units Units.instInv	—	Fintype.sum_equiv mul_comm Units.mul_inv_cancel_right
dft_const_mul 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Ring.toAddCommGroup Pi.Function.module Algebra.toModule Complex.instCommSemiring Ring.toSemiring EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	dft_const_smul IsScalarTower.to_smulCommClass' IsScalarTower.right
dft_const_smul 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass	—	RingHomInvPair.ids Finset.smul_sum Finset.sum_congr SMulCommClass.smul_comm
dft_def 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft Finset.sum Finset.univ fintype SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing commRing AddChar.instFunLike stdAddChar NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids
dft_dft 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Complex.instNatCast NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing	—	—
dft_eq_fourier 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup Pi.Function.module NormedSpace.toModule Complex.instNormedField NormedAddCommGroup.toSeminormedAddCommGroup EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft Fourier.fourierIntegral commRing instMeasurableSpace toCircle MeasureTheory.Measure.count	—	RingHomInvPair.ids Finset.sum_congr MeasureTheory.integral_countable' MeasureTheory.Integrable.of_finite Finite.to_countable Finite.of_fintype instMeasurableSingletonClass MeasureTheory.Measure.count.isFiniteMeasure MeasureTheory.count_real_singleton one_smul tsum_fintype SummationFilter.instLeAtTopUnconditional
dft_even_iff 📖	mathematical	—	Function.Even ZMod Complex NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing DFunLike.coe LinearEquiv Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid AddCommGroup.toAddCommMonoid Complex.addCommGroup Pi.Function.module Complex.instModuleSelf EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft	—	RingHomInvPair.ids dft_comp_neg neg_neg dft_dft IsDomain.toIsCancelMulZero instIsDomain NeZero.charZero Complex.instCharZero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
dft_mul_const 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Ring.toAddCommGroup Pi.Function.module Algebra.toModule Complex.instCommSemiring Ring.toSemiring EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	dft_smul_const IsScalarTower.right
dft_odd_iff 📖	mathematical	—	Function.Odd ZMod Complex NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing Complex.instNeg DFunLike.coe LinearEquiv Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid AddCommGroup.toAddCommMonoid Complex.addCommGroup Pi.Function.module Complex.instModuleSelf EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft	—	RingHomInvPair.ids dft_comp_neg map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass neg_neg dft_dft IsDomain.toIsCancelMulZero instIsDomain NeZero.charZero Complex.instCharZero instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors
dft_smul_const 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dft SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction Ring.toAddCommGroup	—	RingHomInvPair.ids Finset.sum_smul Finset.sum_congr smul_assoc
invDFT_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm dft SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Complex.instInv Complex.instNatCast Finset.sum Finset.univ fintype AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing commRing AddChar.instFunLike stdAddChar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids Finset.sum_congr mul_neg neg_neg
invDFT_apply' 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm dft SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Complex.instInv Complex.instNatCast NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing	—	RingHomInvPair.ids
invDFT_def 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm dft SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Complex.instInv Complex.instNatCast Finset.sum Finset.univ fintype AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing commRing AddChar.instFunLike stdAddChar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHomInvPair.ids invDFT_apply
invDFT_def' 📖	mathematical	—	DFunLike.coe LinearEquiv Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid ZMod AddCommGroup.toAddCommMonoid Pi.Function.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm dft SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Complex.instInv Complex.instNatCast NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing commRing	—	RingHomInvPair.ids

---

← Back to Index