instFiniteIteratedWreathProduct — Mathlib

English

If G is finite, then every IteratedWreathProduct G n is finite (by induction on n).

Русский

Если G конечно, то каждый IteratedWreathProduct G n конечен (индукцией по n).

LaTeX

$$$ [Finite G] :\; \forall n, Finite (IteratedWreathProduct G n) $$$

Lean4

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

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