mathlib

58552fe0 - feat(set_theory/cardinal/basic): cardinality of a powerset (#13786)