theorem proved wrapper

`card_singleton`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  71theorem card_singleton {x : α} : ({x} : Finset α).card = 1 :=

One-line wrapper that applies Finset.card_singleton.

  72  Finset.card_singleton x

From the project-wide theorem graph. These declarations reference this one in their body.

ballFS_card_le_geom in IndisputableMonolith.Causality.ConeBound decl_use
sigma_zero_prime in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use