nat.card status

Stream: general

[Kyle Miller]

(@Bolton Bailey nat.card has been there for a while, but it's little by little seeing more use since you can avoid needing additional fintype and decidable instances, and especially the associated dependent type issues. Inside proofs there are ways to turn things into fintype.card if you need it. There's still API work into it and finite that's on pause due to the porting effort.)

[Yaël Dillies]

Is it really gaining any traction? I've used it less and less.

[Thomas Browning]

I've been using it more and more in finite group theory (one especially nice thing is that you can often drop the finiteness hypothesis for statements like $x^{\lvert G\rvert}=1$ or $\lvert H\rvert\mid\lvert G\rvert$.

[Kyle Miller]

Yaël Dillies said:

Is it really gaining any traction? I've used it less and less.

Yes, library support for it expanded considerably from what there was before a last year, but like I said the porting effort has put any more work into it and other sorts of finiteness on pause.

[Peter Nelson]

Note that, for cardinalities of sets, both mathlib3 and mathlib4 now have set.ncard.