Commit 2024-06-09 12:00 d35039b8

View on Github →

chore(Data/Rat/Cast/Order): Use p, q as variable names (#13644) ... rather than a, b, m, n, r. Also make arguments to rewriting lemmas explicit.

Estimated changes

modified theorem archimedean_iff_rat_lt
modified theorem NNRat.cast_le
modified theorem NNRat.cast_lt
modified theorem NNRat.cast_lt_zero
modified theorem NNRat.cast_max
modified theorem NNRat.cast_min
modified theorem NNRat.cast_nonpos
modified theorem NNRat.cast_pos
modified theorem NNRat.cast_strictMono
modified theorem NNRat.not_cast_lt_zero
modified theorem NNRat.preimage_cast_Icc
modified theorem NNRat.preimage_cast_Ici
modified theorem NNRat.preimage_cast_Ico
modified theorem NNRat.preimage_cast_Iic
modified theorem NNRat.preimage_cast_Iio
modified theorem NNRat.preimage_cast_Ioc
modified theorem NNRat.preimage_cast_Ioi
modified theorem NNRat.preimage_cast_Ioo
modified theorem NNRat.preimage_cast_uIcc
modified theorem NNRat.preimage_cast_uIoc
modified theorem Rat.cast_abs
modified theorem Rat.cast_le
modified theorem Rat.cast_lt
modified theorem Rat.cast_lt_zero
modified theorem Rat.cast_max
modified theorem Rat.cast_min
modified theorem Rat.cast_nonneg
modified theorem Rat.cast_nonpos
modified theorem Rat.cast_pos
modified theorem Rat.cast_pos_of_pos
modified theorem Rat.cast_strictMono
modified theorem Rat.preimage_cast_Icc
modified theorem Rat.preimage_cast_Ici
modified theorem Rat.preimage_cast_Ico
modified theorem Rat.preimage_cast_Iic
modified theorem Rat.preimage_cast_Iio
modified theorem Rat.preimage_cast_Ioc
modified theorem Rat.preimage_cast_Ioi
modified theorem Rat.preimage_cast_Ioo
modified theorem Rat.preimage_cast_uIcc
modified theorem Rat.preimage_cast_uIoc
modified theorem Real.isCauSeq_iff_lift