instGroupIteratedWreathProduct — Mathlib

English

For each n, IteratedWreathProduct G n carries a natural group structure, defined by induction on n.

Русский

Для каждого n есть естественная структура группы на IteratedWreathProduct G n, определяемая по индукции на n.

LaTeX

$$$ [Group G] \Rightarrow \forall n, \text{Group}(\mathrm{IteratedWreathProduct}(G,n)) $$$

Lean4

instance : Group (IteratedWreathProduct G n) := by
  induction n with
  | zero => rw [IteratedWreathProduct_zero]; infer_instance
  | succ n ih => rw [IteratedWreathProduct_succ]; infer_instance

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