Nat

Statistics

Metric	Count
Definitions	0
Theorems `card_preimage_eq_sum_card_image_eq`, `even_sum_iff_even_card_odd`, `odd_sum_iff_odd_card_odd`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`card_preimage_eq_sum_card_image_eq` 📖	mathematical	`Set.Finite` `setOf`	`Nat.card` `Set.Elem` `Set.preimage` `SetLike.coe` `Finset` `instSetLike` `sum` `Nat.instAddCommMonoid`	—	`Set.finite_coe_iff` `Finite.Set.finite_inter_of_left` `Finite.of_fintype` `Set.toFinite_toFinset` `Set.coe_toFinset` `Set.preimage_range` `Set.inter_univ` `sum_subset` `Nat.card_of_isEmpty` `Subtype.isEmpty_false` `Set.Finite.preimage'` `finite_toSet` `Nat.card_eq_card_finite_toFinset` `card_eq_sum_card_image` `sum_congr` `Set.Finite.toFinset.congr_simp` `coe_image` `Set.Finite.coe_toFinset` `Set.image_preimage_eq_inter_range` `ext_iff`
`even_sum_iff_even_card_odd` 📖	mathematical	—	`Even` `sum` `Nat.instAddCommMonoid` `card` `filter` `Odd` `Nat.instSemiring` `Nat.instDecidablePredOdd`	—	`sum_filter_add_sum_filter_not` `Nat.even_add` `Nat.even_iff` `sum_nat_mod` `sum_filter` `sum_congr` `Nat.odd_iff` `card_eq_sum_ones`
`odd_sum_iff_odd_card_odd` 📖	mathematical	—	`Odd` `Nat.instSemiring` `sum` `Nat.instAddCommMonoid` `card` `filter` `Nat.instDecidablePredOdd`	—	`filter.congr_simp`

---