Commit 2024-03-09 10:41 25c53409

View on Github →

chore: resolve (coe : ℤ → α) to ((↑) : ℤ → α) porting notes (#11250) Resolves porting notes claiming "change (coe : ℤ → α) to ((↑) : ℤ → α)" by substituting Int.cast with (↑).

Estimated changes

modified theorem Int.gc_ceil_coe
modified theorem Int.gc_coe_floor
modified theorem Int.preimage_Icc
modified theorem Int.preimage_Ici
modified theorem Int.preimage_Ico
modified theorem Int.preimage_Iic
modified theorem Int.preimage_Iio
modified theorem Int.preimage_Ioc
modified theorem Int.preimage_Ioi
modified theorem Int.preimage_Ioo