Theorems · Theorem · real analysis
Function.Periodic.eq
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddZeroClass α], Function.Periodic f c → f c = f 0- Defined in
- Mathlib.Algebra.Ring.Periodic
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- AddZeroClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- zero_addproof · cited by 2,366
- AddZeroClassstatement and proof · cited by 1,237
- Function.Periodicstatement and proof · cited by 154
Cited by12
Results whose statement or proof uses this declaration.
- Function.Periodic.nat_mul_eqproof · cited by 5
- Function.Periodic.int_mul_eqproof · cited by 5
- Complex.exp_eq_one_iffproof · cited by 3
- Circle.exp_two_piproof · cited by 2
- Function.periodic_iterate_iffproof · cited by 2
- circleIntegral.integral_eq_zero_of_hasDerivWithinAt'proof · cited by 2
- Complex.exp_two_pi_mul_Iproof · cited by 2
- Real.tan_piproof · cited by 1
- Function.Periodic.not_injectiveproof · cited by 1
- Function.Periodic.neg_eqproof · cited by 0
- Function.Periodic.zsmul_eqproof · cited by 0
- Function.Periodic.nsmul_eqproof · cited by 0