card_of_card_eq_four

Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

URI: https://scilib.ai/kg/mathlib#alternatingGroup.card_of_card_eq_four

← MathLib Explorer

English

If Nat.card α = 4, then Nat.card (alternatingGroup α) = 12.

Русский

Если Nat.card α = 4, то Nat.card (alternatingGroup α) = 12.

LaTeX

$$$\text{Nat.card}(alternatingGroup(α)) = 12$$$

Lean4

theorem card_of_card_eq_four (hα4 : Nat.card α = 4) : Nat.card (alternatingGroup α) = 12 :=
  by
  have : Nontrivial α := by
    rw [← Finite.one_lt_card_iff_nontrivial, hα4]
    simp
  rw [nat_card_alternatingGroup, hα4]
  decide

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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