CastCard

Statistics

Metric	Count
Definitions	0
Theorems `cast_card_erase_of_mem`, `cast_card_inter`, `cast_card_sdiff`, `cast_card_union`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_card_erase_of_mem` 📖	mathematical	`Finset` `instMembership`	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `card` `erase` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddMonoidWithOne.toOne`	—	`card_erase_add_one` `Nat.cast_add` `Nat.cast_one` `eq_sub_iff_add_eq`
`cast_card_inter` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `card` `Finset` `instInter` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `instUnion`	—	`eq_sub_iff_add_eq` `Nat.cast_add` `card_inter_add_card_union`
`cast_card_sdiff` 📖	mathematical	`Finset` `instHasSubset`	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `card` `instSDiff` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`card_sdiff_of_subset` `Nat.cast_sub` `card_mono`
`cast_card_union` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `card` `Finset` `instUnion` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `instInter`	—	`eq_sub_iff_add_eq` `Nat.cast_add` `card_union_add_card_inter`

---