card_subtype_diag — Mathlib

English

For a finite α, the number of diag elements in Sym2 α equals card α.

Русский

Для конечного α число диагональных элементов в Sym2 α равно кардинальности α.

LaTeX

$$$|\{ a:\!\ Sym2\alpha \;\mid\; a.IsDiag\}| = |\alpha|$$$

Lean4

theorem card_subtype_diag [Fintype α] : card { a : Sym2 α // a.IsDiag } = card α :=
  by
  convert card_image_diag (univ : Finset α)
  rw [← filter_image_mk_isDiag, Fintype.card_of_subtype]
  rintro x
  rw [mem_filter, univ_product_univ, mem_image]
  obtain ⟨a, ha⟩ := Quot.exists_rep x
  exact and_iff_right ⟨a, mem_univ _, ha⟩

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