minimalPeriod_snd_dvd — Mathlib

English

The minimal period of the second component under g divides the minimal period of Prod.map f g at x.

Русский

Минимальный период второй компоненты при g делит минимальный период отображения Prod.map f g в точке x.

LaTeX

$$$\operatorname{minimalPeriod} g x.2 \mid \operatorname{minimalPeriod}(\operatorname{Prod.map} f g) x$$$

Lean4

theorem minimalPeriod_snd_dvd : minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x := by rw [minimalPeriod_prodMap];
  exact Nat.dvd_lcm_right _ _

Похожие утверждения