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 SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SummationFilter.unconditional	—	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	38 math math: Circle.periodic_exp, toIocMod_periodic, Antiperiodic.div, Real.sin_periodic, Nat.periodic_coprime, Nat.periodic_mod, Antiperiodic.periodic_two_mul, Antiperiodic.int_even_mul_periodic, AddCircle.scaled_exp_map_periodic, IsMIntegralCurve.periodic_xor_injective, Antiperiodic.periodic, periodic_with_period_zero, PeriodPair.periodic_derivWeierstrassP, Complex.exp_periodic, Antiperiodic.nat_even_mul_periodic, Antiperiodic.mul, ContinuousMap.periodic_tsum_comp_add_zsmul, SlashInvariantFormClass.periodic_comp_ofComplex, Int.fract_periodic, Real.tan_periodic, periodic_circleMap, Complex.cos_periodic, Nat.periodic_gcd, Complex.sin_periodic, Real.cos_periodic, IsPeriodicPt.periodic_iterate, Complex.circleTransformDeriv_periodic, Antiperiodic.even_zsmul_periodic, Antiperiodic.add, toIcoMod_periodic, Antiperiodic.even_nsmul_periodic, PeriodPair.periodic_weierstrassP, Antiperiodic.sub, Complex.tan_periodic, periodic_iterate_iff, Complex.exp_mul_I_periodic, Real.Angle.tan_periodic, IsMIntegralCurve.periodic_of_eq

---

← Back to Index