Commit 2023-01-27 06:03 f7aeed7f

View on Github →

feat: port Data.Int.Interval (#1869)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Hom/Embedding.lean

Created Mathlib/Data/Int/Interval.lean

added theorem Int.Icc_eq_finset_map

added theorem Int.Ico_eq_finset_map

added theorem Int.Ioc_eq_finset_map

added theorem Int.Ioo_eq_finset_map

added theorem Int.card_Icc

added theorem Int.card_Icc_of_le

added theorem Int.card_Ico

added theorem Int.card_Ico_of_le

added theorem Int.card_Ioc

added theorem Int.card_Ioc_of_le

added theorem Int.card_Ioo

added theorem Int.card_Ioo_of_lt

added theorem Int.card_fintype_Icc

added theorem Int.card_fintype_Icc_of_le

added theorem Int.card_fintype_Ico

added theorem Int.card_fintype_Ico_of_le

added theorem Int.card_fintype_Ioc

added theorem Int.card_fintype_Ioc_of_le

added theorem Int.card_fintype_Ioo

added theorem Int.card_fintype_Ioo_of_lt

added theorem Int.image_Ico_emod