Card

📁 Source: Mathlib/Data/Setoid/Partition/Card.lean

Statistics

Metric	Count
Definitions	0
Theorems ncard_eq_finsum	1
Total	1

Setoid.IsPartition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ncard_eq_finsum 📖	mathematical	Setoid.IsPartition	Set.ncard finsum Set.Elem Set Nat.instAddCommMonoid Set.instInter Set.instMembership	—	Set.Finite.inter_of_left Nat.card_eq_card_finite_toFinset Set.nonempty_of_ncard_ne_zero Subtype.prop Finite.of_injective ExistsUnique.unique finsum_def Finset.sum_congr Finset.card_sigma Finset.card_nbij' ExistsUnique.exists Finset.coe_sigma Set.Finite.coe_toFinset Nat.card_ne_zero

---

← Back to Index