offDiag_card — Mathlib

English

The off-diagonal has size |S|^2 − |S|.

Русский

Размер вне диагонали равен |S|^2 − |S|.

LaTeX

$$$|\\mathrm{offDiag}(s)| = |s|^2 - |s|$$$

Lean4

@[simp]
theorem offDiag_card : (offDiag s).card = s.card * s.card - s.card :=
  suffices (diag s).card + (offDiag s).card = s.card * s.card by rw [s.diag_card] at this; cutsat
  by
  rw [← card_product, diag, offDiag]
  conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]

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