comp_addHom — Mathlib

English

If f is periodic with c and g is an AddHom γ α with a right inverse g_inv, then f ∘ g is periodic with period g_inv(c).

Русский

Если f периодична с периодом c, и g — AddHom γ α с правым обратным g_inv, тогда f ∘ g периодична с периодом g_inv(c).

LaTeX

$$$\mathrm{Periodic}(f \circ g, g_{inv}(c))$ under the given hypotheses.$$

Lean4

theorem comp_addHom [Add α] [Add γ] (h : Periodic f c) (g : AddHom γ α) (g_inv : α → γ) (hg : RightInverse g_inv g) :
    Periodic (f ∘ g) (g_inv c) := fun x => by simp only [hg c, h (g x), map_add, comp_apply]

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