Commit 2024-03-15 12:53 ebabd046

View on Github →

feat: counting elements in an interval with given residue (#9348)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/CardIntervalMod.lean

added theorem Int.Ico_filter_dvd_card

added theorem Int.Ico_filter_dvd_eq

added theorem Int.Ico_filter_modEq_card

added theorem Int.Ico_filter_modEq_eq

added theorem Int.Ioc_filter_dvd_card

added theorem Int.Ioc_filter_dvd_eq

added theorem Int.Ioc_filter_modEq_card

added theorem Int.Ioc_filter_modEq_eq

added theorem Nat.Ico_filter_modEq_card

added theorem Nat.Ico_filter_modEq_cast

added theorem Nat.Ioc_filter_modEq_card

added theorem Nat.Ioc_filter_modEq_cast

added theorem Nat.count_modEq_card

added theorem Nat.count_modEq_card_eq_ceil