Commit 2026-01-03 16:31 96123a30

View on Github →

feat(ToIntervalMod): add missing lemmas (#33442) Cherry-picked from #33423, then added more lemmas as requested by @eric-wieser

Estimated changes

added theorem self_sub_toIcoDiv_mul
added theorem self_sub_toIocDiv_mul
added theorem toIcoDiv_add_nsmul'
added theorem toIcoDiv_add_nsmul
added theorem toIcoDiv_add_ofNat_mul
added theorem toIcoDiv_eq_iff
added theorem toIcoDiv_mul_sub_self
added theorem toIcoDiv_nsmul_add
added theorem toIcoDiv_ofNat_mul_add
added theorem toIcoDiv_sub_nsmul'
added theorem toIcoDiv_sub_nsmul
added theorem toIcoDiv_sub_ofNat_mul
added theorem toIcoMod_add_nsmul'
added theorem toIcoMod_add_nsmul
added theorem toIcoMod_add_ofNat_mul
added theorem toIcoMod_nsmul_add'
added theorem toIcoMod_nsmul_add
added theorem toIcoMod_ofNat_mul_add
added theorem toIcoMod_sub_nsmul'
added theorem toIcoMod_sub_nsmul
added theorem toIcoMod_sub_ofNat_mul
added theorem toIocDiv_add_nsmul'
added theorem toIocDiv_add_nsmul
added theorem toIocDiv_add_ofNat_mul
added theorem toIocDiv_eq_iff
added theorem toIocDiv_mul_sub_self
added theorem toIocDiv_nsmul_add
added theorem toIocDiv_ofNat_mul_add
added theorem toIocDiv_sub_nsmul'
added theorem toIocDiv_sub_nsmul
added theorem toIocDiv_sub_ofNat_mul
added theorem toIocMod_add_nsmul'
added theorem toIocMod_add_nsmul
added theorem toIocMod_add_ofNat_mul
added theorem toIocMod_nsmul_add'
added theorem toIocMod_nsmul_add
added theorem toIocMod_ofNat_mul_add
added theorem toIocMod_sub_nsmul'
added theorem toIocMod_sub_nsmul
added theorem toIocMod_sub_ofNat_mul