Theorems · Theorem · dynamical systems
Function.minimalPeriod_piMap
∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → α i → α i} {x : (i : ι) → α i},
Function.minimalPeriod (Pi.map f) x = sInf {n | n > 0 ∧ ∀ (i : ι), Function.minimalPeriod (f i) (x i) ∣ n}This sInf can be regarded as a generalized version of LCM
for possibly infinite sets and types.
- Defined in
- Mathlib.Dynamics.PeriodicPts.Lemmas
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.ofPredstatement and proof · cited by 6,101
- InfSet.sInfstatement and proof · cited by 935
- Function.minimalPeriodstatement and proof · cited by 100
- Function.IsPeriodicPtproof · cited by 68
- Pi.mapstatement and proof · cited by 60
- Function.minimalPeriod_eq_sInf_n_pos_IsPeriodicPtproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- Function.minimalPeriod_single_dvd_minimalPeriod_piMapproof · cited by 2
- Pi.addOrderOf_eq_sInfproof · cited by 0
- Pi.orderOf_eq_sInfproof · cited by 0