comp_pow — Mathlib

English

Let f: X → M and h: Y → X. Then h followed by the n-th power of f equals the n-th power of the composition: h ∘ f^n = (h ∘ f)^n for all n ∈ ℕ.

Русский

Пусть f: X → M и h: Y → X. Тогда h ∘ f^n = (h ∘ f)^n для всех n ∈ ℕ.

LaTeX

$$$ h \\circ f^n = (h \\circ f)^n \\quad (n \\in \\mathbb{N}) $$$

Lean4

@[reassoc]
theorem comp_pow (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X) : h ≫ f ^ n = (h ≫ f) ^ n := by
  induction n <;> simp [pow_succ, MonObj.comp_mul, *]

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