Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-23 10:32 aeb7facf

View on Github →

feat(data/rat/cast): add lemmas, golf (#16194)

  • add rat.cast_strict_mono, rat.cast_strict_mono, and rat.cast_order_embedding;
  • use these lemmas to prove rat.cast_le etc;
  • add rat.preimage_cast_Ixx.

Estimated changes

modified theorem rat.cast_abs
added theorem rat.cast_eq_id
modified theorem rat.cast_hom_rat
modified theorem rat.cast_id
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
added theorem rat.cast_mono
modified theorem rat.cast_nonneg
modified theorem rat.cast_nonpos
modified theorem rat.cast_pos
added theorem rat.cast_pos_of_pos
added theorem rat.cast_strict_mono
added theorem rat.preimage_cast_Icc
added theorem rat.preimage_cast_Ici
added theorem rat.preimage_cast_Ico
added theorem rat.preimage_cast_Iic
added theorem rat.preimage_cast_Iio
added theorem rat.preimage_cast_Ioc
added theorem rat.preimage_cast_Ioi
added theorem rat.preimage_cast_Ioo