card — Mathlib

English

For finite Q, the cardinality of the regular wreath product is |D|^{|Q|} · |Q|.

Русский

Для конечного множества Q кардинал регулярного вентового произведения равен |D|^{|Q|} · |Q|.

LaTeX

$$$ \#(D \wr_{\mathrm{r}} Q) = \#D^{\#Q} \cdot \#Q $$$

Lean4

theorem card [Finite Q] : Nat.card (D ≀ᵣ Q) = Nat.card D ^ Nat.card Q * Nat.card Q := by
  rw [Nat.card_congr (equivProd D Q), Nat.card_prod (Q → D) Q, Nat.card_fun]

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