Commit 2023-07-17 02:18 ae594c90

View on Github →

feat: finset.uIcc on concrete structures (#5946) Match https://github.com/leanprover-community/mathlib/pull/18838

Estimated changes

added theorem DFinsupp.card_uIcc
added theorem Fin.card_fintype_uIcc
added theorem Fin.card_uIcc
added theorem Fin.coe_inf
added theorem Fin.coe_max
added theorem Fin.coe_min
added theorem Fin.coe_sup
added theorem Finsupp.Icc_eq
added theorem Finsupp.card_uIcc
deleted theorem Finsupp.icc_eq
modified theorem Int.card_Icc
modified theorem Int.card_Ico
modified theorem Int.card_Ioc
modified theorem Int.card_Ioo
added theorem Int.card_fintype_uIcc
added theorem Int.card_uIcc
added theorem Int.uIcc_eq_finset_map
modified theorem Multiset.card_Iic
added theorem Multiset.card_uIcc
added theorem Multiset.uIcc_eq
added theorem Nat.card_uIcc
added theorem Nat.uIcc_eq_range'
added theorem PNat.card_fintype_uIcc
added theorem PNat.card_uIcc
added theorem Pi.card_uIcc
added theorem Pi.uIcc_eq
added theorem Set.finite_interval