English
For x = (a,b) in α × β, the minimal period of Prod.map f g at x equals the least common multiple of the minimal periods of f at a and g at b: minimalPeriod(Prod.map f g) x = lcm(minimalPeriod f a, minimalPeriod g b).
Русский
Для пары x=(a,b) в произведении α×β минимальный период отображения Prod.map f g в точке x равен НОК минимальных периодов f в a и g в b.
LaTeX
$$$\operatorname{minimalPeriod}(\operatorname{Prod.map} f g) x = \operatorname{lcm}(\operatorname{minimalPeriod} f x.1, \operatorname{minimalPeriod} g x.2)$$$
Lean4
theorem minimalPeriod_prodMap (f : α → α) (g : β → β) (x : α × β) :
minimalPeriod (Prod.map f g) x = (minimalPeriod f x.1).lcm (minimalPeriod g x.2) :=
eq_of_forall_dvd <| by simp [← isPeriodicPt_iff_minimalPeriod_dvd, Nat.lcm_dvd_iff]
