Commit 2025-02-08 16:01 6c3546e9

feat: missing basic API lemmas for Nat.card, Fintype.card (#20131) card_sigma existed for Fintype.card and I've added it for Nat.card. This version uses Finite instead of Fintype for the dependent type, for generality. card_univ existed for Nat.card and I've added it for Fintype.card. I've added card_subtype_true for both Nat.card and Fintype.card. I've renamed empty_card -> card_empty With Fintype.card rewrite lemmas, one has to be careful about the instance to avoid unifying with a non-defeq instance. This can be solved by taking the instance as a (normal) implicit parameter. However, it is not clear that this is really necessary.