Periodic

📁 Source: Mathlib/Topology/ContinuousMap/Periodic.lean

Statistics

Metric	Count
Definitions Periodic	1
Theorems periodic_tsum_comp_add_zsmul	1
Total	2

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
periodic_tsum_comp_add_zsmul 📖	mathematical	—	Function.Periodic AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid DFunLike.coe ContinuousMap instFunLike tsum instAddCommMonoidOfContinuousAdd compactOpen comp addRight instSeparatelyContinuousAddOfContinuousAdd SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SummationFilter.unconditional	—	instSeparatelyContinuousAddOfContinuousAdd Equiv.summable_iff tsum_apply SummationFilter.instNeBotUnconditional addRight.congr_simp add_one_zsmul add_comm Equiv.tsum_eq tsum_eq_zero_of_not_summable

Function

Definitions

Name	Category	Theorems
Periodic 📖	MathDef	75 math math: Circle.periodic_exp, Periodic.sub_const, toIocMod_periodic, Antiperiodic.div, Periodic.int_mul, Real.sin_periodic, Nat.periodic_coprime, Nat.periodic_mod, Antiperiodic.periodic_two_mul, List.periodic_prod, Periodic.nsmul, Antiperiodic.int_even_mul_periodic, Finset.periodic_prod, Periodic.mul_const', AddCircle.scaled_exp_map_periodic, IsMIntegralCurve.periodic_xor_injective, Antiperiodic.periodic, periodic_with_period_zero, Periodic.nat_mul, Multiset.periodic_sum, Finset.periodic_sum, Periodic.comp_addHom, Periodic.div_const, PeriodPair.periodic_derivWeierstrassP, Periodic.add_const, Complex.exp_periodic, Antiperiodic.nat_even_mul_periodic, Antiperiodic.mul, ContinuousMap.periodic_tsum_comp_add_zsmul, SlashInvariantFormClass.periodic_comp_ofComplex, Int.fract_periodic, Periodic.neg, Periodic.const_add, Multiset.periodic_prod, Periodic.div, Real.tan_periodic, periodic_circleMap, Complex.cos_periodic, Nat.periodic_gcd, Periodic.const_smul₀, Complex.sin_periodic, Periodic.vadd, Periodic.add, Periodic.const_inv_mul, Periodic.comp, Periodic.mul_const_inv, Real.cos_periodic, List.periodic_sum, IsPeriodicPt.periodic_iterate, Complex.circleTransformDeriv_periodic, Antiperiodic.even_zsmul_periodic, Antiperiodic.add, toIcoMod_periodic, Periodic.zsmul, Antiperiodic.even_nsmul_periodic, PeriodPair.periodic_weierstrassP, Periodic.smul, Periodic.const_smul, Antiperiodic.sub, Periodic.mul_const, Complex.tan_periodic, periodic_iterate_iff, Periodic.mul, Complex.exp_mul_I_periodic, Periodic.sub, Periodic.neg_nat_mul, Real.Angle.tan_periodic, IsMIntegralCurve.periodic_of_eq, Periodic.const_mul, Periodic.add_period, Periodic.const_inv_smul₀, Periodic.sub_period, Periodic.const_sub, Periodic.const_inv_smul, Periodic.neg_nsmul

---

← Back to Index