Order

Stream: mathlib4

[vxctyxeha]

how to prove this

import Mathlib                      -- 避免 lint 错误 (有时需要)

open Subgroup Equiv Equiv.Perm Finset Nat List

abbrev S4 : Type := Perm (Fin 4)


lemma card : Nat.card S4 = 24 := by
  sorry

[Niels Voss]

lemma card : Nat.card S4 = 24 := by
  aesop

works for me. If you want to do it manually, you can do

lemma card : Nat.card S4 = 24 := by
  unfold S4
  rw [Nat.card_perm, Nat.card_eq_fintype_card, Fintype.card_fin]
  rfl