card — Mathlib

English

If G is finite, then Nat.card (IteratedWreathProduct G n) = Nat.card G ^ (sum_{i=0}^{n-1} Nat.card G ^ i).

Русский

Если G конечно, то кардинал IteratedWreathProduct G n равен |G|^{sum_{i=0}^{n-1} |G|^i}.

LaTeX

$$$ \operatorname{Nat.card}(\mathrm{IteratedWreathProduct}(G,n)) = \operatorname{Nat.pow}(\operatorname{Nat.card} G) \Big(\sum_{i=0}^{n-1} \operatorname{Nat.card} G^{i} \Big) $$$

Lean4

theorem card [Finite G] : Nat.card (IteratedWreathProduct G n) = Nat.card G ^ (∑ i ∈ Finset.range n, Nat.card G ^ i) :=
  by
  induction n with
  | zero => simp
  | succ n h => rw [IteratedWreathProduct_succ, RegularWreathProduct.card, h, geom_sum_succ, pow_succ, pow_mul']

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