Commit 2026-05-10 13:51 08fe4f24
View on Github →feat: the cardinal of a finset is an ite sum over a bigger finset (#37831)
If s ⊆ t then s.card = ∑ i ∈ t, if i ∈ s then 1 else 0.
feat: the cardinal of a finset is an ite sum over a bigger finset (#37831)
If s ⊆ t then s.card = ∑ i ∈ t, if i ∈ s then 1 else 0.