IteratedWreathProduct_succ

Mathlib.GroupTheory.RegularWreathProduct

URI: https://scilib.ai/kg/mathlib#IteratedWreathProduct_succ

English

The successor step satisfies IteratedWreathProduct G (n+1) = (IteratedWreathProduct G n) ≀ᵣ G.

Русский

Переход к следующему шагу: IteratedWreathProduct G (n+1) = (IteratedWreathProduct G n) ≀ᵣ G.

LaTeX

$$$ IteratedWreathProduct(G,n+1) = IteratedWreathProduct(G,n) \wr_{\mathrm{r}} G $$$

Lean4

@[simp]
theorem IteratedWreathProduct_succ : IteratedWreathProduct G (n + 1) = (IteratedWreathProduct G n) ≀ᵣ G :=
  rfl

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

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

Разделы

Аффилиация

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