commute_pow_left_of_commute — Mathlib

English

If g2 commutes with g via h (i.e., g2 ∘ f = f ∘ g), then (g2^k) ∘ f = f ∘ (g^k) for all k ∈ N.

Русский

Если g2 коммутирует с g через h (g2 ∘ f = f ∘ g), тогда для любого k ∈ N выполняется (g2^k) ∘ f = f ∘ (g^k).

LaTeX

$$$(g_2^k) \\circ f = f \\circ (g^k) \\quad \\text{for } k \\in \\mathbb{N},$ при условии $g_2 \\circ f = f \\circ g$.$$

Lean4

theorem commute_pow_left_of_commute [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {f : M →ₛₗ[σ₁₂] M₂}
    {g : Module.End R M} {g₂ : Module.End R₂ M₂} (h : g₂.comp f = f.comp g) (k : ℕ) :
    (g₂ ^ k).comp f = f.comp (g ^ k) := by
  induction k with
  | zero => simp [one_eq_id]
  | succ k ih =>
    rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih, ← LinearMap.comp_assoc, h, LinearMap.comp_assoc,
      mul_eq_comp]

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