comp_zpow

Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_

URI: https://scilib.ai/kg/mathlib#GrpObj.comp_zpow

← MathLib Explorer

English

For arrows f: X→Y and g: Y→G, and any integer n, f∘g^n = (f∘g)^n.

Русский

Для стрел f:X→Y, g:Y→G и любого целого n выполняется f∘g^n = (f∘g)^n.

LaTeX

$$f \circ g^n = (f \circ g)^n$$

Lean4

@[reassoc]
theorem comp_zpow (f : X ⟶ Y) (g : Y ⟶ G) : ∀ n : ℤ, f ≫ g ^ n = (f ≫ g) ^ n
  | (n : ℕ) => by simp [comp_pow]
  | .negSucc n => by simp [comp_pow, comp_inv]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru