map_comp_zpow' — Mathlib

English

For any g : ι → G and n ∈ ℤ, f ∘ (g^n) = (f ∘ g)^n, provided hf: ∀ x, f x⁻¹ = (f x)⁻¹.

Русский

Для любого g : ι → G и целого n, выполняется f ∘ (g^n) = (f ∘ g)^n при условии hf: ∀ x, f x⁻¹ = (f x)⁻¹.

LaTeX

$$$$ \forall g: \iota \to G,\ \forall n \in \mathbb{Z},\ f \circ (g^n) = (f \circ g)^n. $$$$

Lean4

@[to_additive (attr := simp)]
theorem map_comp_zpow' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F) (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹)
    (g : ι → G) (n : ℤ) : f ∘ (g ^ n) = f ∘ g ^ n := by ext; simp [map_zpow' f hf]

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