pow_comp — Mathlib

English

For a monoid object M, and morphisms f: X → M, g: M → N, the powers commute with composition: (f^n) ≫ g = (f ≫ g)^n.

Русский

Для моноидного объекта M и морфизмов f: X → M, g: M → N, степени сохраняют композицию: (f^n) ≫ g = (f ≫ g)^n.

LaTeX

$$$ (f^{n}) \\; \\circ g = (f \\circ g)^{n} $$$

Lean4

@[reassoc]
theorem pow_comp (f : X ⟶ M) (n : ℕ) (g : M ⟶ N) [IsMonHom g] : (f ^ n) ≫ g = (f ≫ g) ^ n := by
  induction n <;> simp [pow_succ, MonObj.mul_comp, *]

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