Commit 2024-11-25 17:50 b98172a9

View on Github →

feat: Icc a b + Icc c d = Icc (a + c) (b + d) (#19398) From GrowthInGroups Moves:

  • inv_Ioi -> inv_Ioi₀

Estimated changes

added theorem Set.Icc_mul_Icc
added theorem Set.inv_Icc
added theorem Set.inv_Ici
added theorem Set.inv_Ico
added theorem Set.inv_Iic
added theorem Set.inv_Iio
added theorem Set.inv_Ioc
modified theorem Set.inv_Ioi
added theorem Set.inv_Ioi₀
added theorem Set.inv_Ioo
added theorem Set.inv_uIcc
deleted theorem Set.preimage_neg_Icc
deleted theorem Set.preimage_neg_Ici
deleted theorem Set.preimage_neg_Ico
deleted theorem Set.preimage_neg_Iic
deleted theorem Set.preimage_neg_Iio
deleted theorem Set.preimage_neg_Ioc
deleted theorem Set.preimage_neg_Ioi
deleted theorem Set.preimage_neg_Ioo
modified theorem Set.preimage_neg_uIcc
added theorem Set.smul_Icc