mem_alternatingGroup

Mathlib.GroupTheory.SpecificGroups.Alternating

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.mem_alternatingGroup

English

For card α = 4, |kleinFour(α)| = 4.

Русский

При card(α) = 4, |kleinFour(α)| = 4.

LaTeX

$$$\lvert \mathrm{kleinFour}(\alpha) \rvert = 4$$$

Lean4

@[simp]
theorem mem_alternatingGroup {f : Perm α} : f ∈ alternatingGroup α ↔ sign f = 1 :=
  sign.mem_ker

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

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

Разделы

Аффилиация

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