card_index_eq_twelve — Mathlib

English

The index set ι has exactly 12 elements: |ι| = 12.

Русский

Множество индексов ι содержит ровно 12 элементов: |ι| = 12.

LaTeX

$$Nat.card ι = 12$$

Lean4

theorem card_index_eq_twelve : Nat.card ι = 12 := by
  classical
  have this : Nat.card (allRoots P).toFinset = 12 :=
    by
    rw [Nat.card_eq_fintype_card, Fintype.card_coe, toFinset_card_of_nodup (allRoots_nodup P)]
    simp
  rw [← this]
  exact Nat.card_congr <| indexEquivAllRoots P

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