Commit 2025-03-06 15:53 605e60a0

View on Github →

chore(Data/Fintype/Card): assume Fintype {a // p a} instead of deriving it from DecidablePred p (#22643) This makes the lemmas more syntactically general From PlainCombi (LeanCamCombi)

Estimated changes

modified theorem Fintype.card_subtype
modified theorem Fintype.card_subtype_le
modified theorem Fintype.card_subtype_lt