cardCommutatorBound — Mathlib

English

A formal bound function cardCommutatorBound(n) gives an upper bound for the size of the commutator subgroup in terms of n = card(commutatorSet G).

Русский

Функция cardCommutatorBound(n) задаёт верхнюю границу размера коммутаторной подгруппы по n = card(commutatorSet G).

LaTeX

$$cardCommutatorBound(n) = (n^(2n))^(n^(2n+1) + 1)$$

Lean4

/-- A bound for the size of the commutator subgroup in terms of the number of commutators. -/
def cardCommutatorBound (n : ℕ) :=
  (n ^ (2 * n)) ^ (n ^ (2 * n + 1) + 1)

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