instFinite

Mathlib.GroupTheory.RegularWreathProduct

URI: https://scilib.ai/kg/mathlib#RegularWreathProduct.instFinite

English

If D and Q are finite (in particular Q is finite and thus D is finite as needed), then the regular wreath product D ≀ᵣ Q is finite.

Русский

Если D и Q конечны, то регулярное вентовое произведение D ≀ᵣ Q конечно.

LaTeX

$$$\text{Finite}(D \wr_{\mathrm{r}} Q)$$$

Lean4

instance [Finite D] [Finite Q] : Finite (D ≀ᵣ Q) :=
  Finite.of_equiv _ (equivProd D Q).symm

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

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

Разделы

Аффилиация

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