PontryaginDuality

📁 Source: Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean

Statistics

Metric	Count
Definitions circleEquivComplex, complexBasis, doubleDualEquiv, zmodAddEquiv, zmodHom	5
Theorems card_eq, coe_complexBasis, coe_doubleDualEquiv, complexBasis_apply, doubleDualEmb_bijective, doubleDualEmb_doubleDualEquiv_symm_apply, doubleDualEmb_eq_zero, doubleDualEmb_inj, doubleDualEmb_injective, doubleDualEmb_ne_zero, doubleDualEquiv_symm_doubleDualEmb_apply, exists_apply_ne_zero, expect_apply_eq_ite, expect_apply_eq_zero_iff_ne_zero, expect_apply_ne_zero_iff_eq_zero, forall_apply_eq_zero, sum_apply_eq_ite, sum_apply_eq_zero_iff_ne_zero, sum_apply_ne_zero_iff_eq_zero, zmodAddEquiv_apply, zmod_add, zmod_inj, zmod_injective, zmod_intCast, zmod_zero	25
Total	30

AddChar

Definitions

Name	Category	Theorems
circleEquivComplex 📖	CompOp	1 math math: zmodAddEquiv_apply
complexBasis 📖	CompOp	2 math math: coe_complexBasis, complexBasis_apply
doubleDualEquiv 📖	CompOp	3 math math: coe_doubleDualEquiv, doubleDualEquiv_symm_doubleDualEmb_apply, doubleDualEmb_doubleDualEquiv_symm_apply
zmodAddEquiv 📖	CompOp	1 math math: zmodAddEquiv_apply
zmodHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq 📖	mathematical	—	Fintype.card AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring instFintype Complex.instRCLike Finite.of_fintype	—	Finite.of_fintype AddCommGroup.equiv_directSum_zmod_of_finite' ne_of_gt lt_trans Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass AddEquiv.injective compAddMonoidHom_injective_left AddEquiv.surjective DFunLike.coe_injective Equiv.injective LE.le.antisymm card_addChar_le Fintype.card_le_of_injective
coe_complexBasis 📖	mathematical	—	DFunLike.coe Module.Basis AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module Complex.instModuleSelf Module.Basis.instFunLike complexBasis instFunLike	—	linearIndependent complexBasis.eq_1 coe_basisOfLinearIndependentOfCardEqFinrank
coe_doubleDualEquiv 📖	mathematical	—	DFunLike.coe AddEquiv AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring instAddCommGroup CommRing.toCommMonoid Complex.commRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommMonoid EquivLike.toFunLike AddEquiv.instEquivLike doubleDualEquiv AddMonoidHom CommMonoid.toMonoid AddCommMonoid.toAddMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike doubleDualEmb	—	—
complexBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Pi.Function.module Complex.instModuleSelf Module.Basis.instFunLike complexBasis instFunLike	—	coe_complexBasis
doubleDualEmb_bijective 📖	mathematical	—	Function.Bijective AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex CommMonoid.toMonoid CommRing.toCommMonoid Complex.commRing AddCommMonoid.toAddMonoid instAddCommMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike doubleDualEmb	—	nonempty_fintype Finite.of_fintype Fintype.bijective_iff_injective_and_card doubleDualEmb_injective card_eq
doubleDualEmb_doubleDualEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex CommMonoid.toMonoid CommRing.toCommMonoid Complex.commRing AddCommMonoid.toAddMonoid instAddCommMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike doubleDualEmb AddEquiv MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring instAddCommGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm doubleDualEquiv	—	AddEquiv.apply_symm_apply
doubleDualEmb_eq_zero 📖	mathematical	—	DFunLike.coe AddMonoidHom AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex CommMonoid.toMonoid CommRing.toCommMonoid Complex.commRing AddCommMonoid.toAddMonoid instAddCommMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike doubleDualEmb instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
doubleDualEmb_inj 📖	mathematical	—	DFunLike.coe AddMonoidHom AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex CommMonoid.toMonoid CommRing.toCommMonoid Complex.commRing AddCommMonoid.toAddMonoid instAddCommMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike doubleDualEmb	—	doubleDualEmb_injective
doubleDualEmb_injective 📖	mathematical	—	AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex CommMonoid.toMonoid CommRing.toCommMonoid Complex.commRing AddCommMonoid.toAddMonoid instAddCommMonoid DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike doubleDualEmb	—	AddMonoidHom.ker_eq_bot_iff eq_bot_iff forall_apply_eq_zero DFunLike.congr_fun
doubleDualEmb_ne_zero 📖	—	—	—	—	Iff.not doubleDualEmb_eq_zero
doubleDualEquiv_symm_doubleDualEmb_apply 📖	mathematical	—	DFunLike.coe AddEquiv AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring instAddCommGroup CommRing.toCommMonoid Complex.commRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid AddCommGroup.toAddCommMonoid EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm doubleDualEquiv Finite.of_fintype instFintype Complex.instRCLike AddMonoidHom CommMonoid.toMonoid AddCommMonoid.toAddMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike doubleDualEmb	—	AddEquiv.symm_apply_apply Finite.of_fintype
exists_apply_ne_zero 📖	—	—	—	—	map_zero_eq_one RingHomInvPair.ids Module.Basis.sum_repr one_ne_zero NeZero.charZero_one Complex.instCharZero Finset.sum_congr complexBasis_apply Fintype.sum_apply mul_one
expect_apply_eq_ite 📖	mathematical	—	Finset.expect AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield Complex.instField Complex.instCharZero Finset.univ instFintype Complex.instRCLike DFunLike.coe instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Complex.instOne Complex.instZero	—	Complex.instCharZero Finset.expect_congr expect_eq_ite instIsDomain
expect_apply_eq_zero_iff_ne_zero 📖	mathematical	—	Finset.expect AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Algebra.toModule NNRat instCommSemiringNNRat DivisionSemiring.toNNRatAlgebra Semifield.toDivisionSemiring Field.toSemifield Complex.instField Complex.instCharZero Finset.univ instFintype Complex.instRCLike DFunLike.coe instFunLike Complex.instZero	—	nonempty_fintype Complex.instCharZero expect_apply_eq_ite Ne.ite_eq_right_iff one_ne_zero NeZero.charZero_one
expect_apply_ne_zero_iff_eq_zero 📖	mathematical	—	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Iff.not_left Complex.instCharZero expect_apply_eq_zero_iff_ne_zero
forall_apply_eq_zero 📖	mathematical	—	DFunLike.coe AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring instFunLike Complex.instOne NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Iff.not exists_apply_ne_zero
sum_apply_eq_ite 📖	mathematical	—	Finset.sum AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finset.univ instFintype Complex.instRCLike Finite.of_fintype DFunLike.coe instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Complex.instNatCast Fintype.card Complex.instZero	—	Finite.of_fintype Finset.sum_congr card_eq sum_eq_ite instIsDomain
sum_apply_eq_zero_iff_ne_zero 📖	mathematical	—	Finset.sum AddChar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finset.univ instFintype Complex.instRCLike DFunLike.coe instFunLike Complex.instZero	—	nonempty_fintype Finite.of_fintype sum_apply_eq_ite Ne.ite_eq_right_iff Nat.cast_ne_zero Complex.instCharZero Fintype.card_ne_zero AddTorsor.nonempty
sum_apply_ne_zero_iff_eq_zero 📖	mathematical	—	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Iff.not_left sum_apply_eq_zero_iff_ne_zero
zmodAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv ZMod AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing Complex MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instAddCommMonoid CommRing.toCommMonoid Complex.commRing EquivLike.toFunLike AddEquiv.instEquivLike zmodAddEquiv SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.toAddCommGroup Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup CommGroup.toCommMonoid circleEquivComplex Finite.of_fintype ZMod.fintype zmod	—	—
zmod_add 📖	mathematical	—	zmod ZMod Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass instCommGroup Ring.toAddCommGroup CommGroup.toCommMonoid	—	add_mul Distrib.rightDistribClass map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass map_add_eq_mul
zmod_inj 📖	mathematical	—	zmod	—	zmod_injective
zmod_injective 📖	mathematical	—	ZMod AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup zmod	—	Function.Surjective.forall ZMod.intCast_surjective NeZero.charZero RCLike.charZero_rclike CharP.intCast_eq_intCast ZMod.charP Nat.instAtLeastTwoHAddOfNat Int.cast_one mul_one NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass div_self one_mul zmod_intCast DFunLike.congr_fun
zmod_intCast 📖	mathematical	—	DFunLike.coe AddChar ZMod AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup instFunLike zmod AddGroupWithOne.toIntCast ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceCircle ContinuousMap.instFunLike Circle.exp Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi DivInvMonoid.toDiv Real.instDivInvMonoid Real.instIntCast	—	Nat.instAtLeastTwoHAddOfNat Int.cast_mul ZMod.toAddCircle_intCast div_one
zmod_zero 📖	mathematical	—	zmod ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Circle DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Circle.instCommGroup instOne	—	DFunLike.ext MulZeroClass.zero_mul map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass map_zero_eq_one

---

← Back to Index