Commit 2025-08-24 17:49 1f5ee2b5

View on Github →

feat(Rat/Lemmas): add lemmas about (q ± n).den (#28809)

Estimated changes

modified theorem Rat.add_den_dvd
added theorem Rat.add_intCast_den
added theorem Rat.add_natCast_den
added theorem Rat.add_ofNat_den
added theorem Rat.intCast_add_den
added theorem Rat.intCast_sub_den
added theorem Rat.natCast_add_den
added theorem Rat.natCast_sub_den
added theorem Rat.ofNat_add_den
added theorem Rat.ofNat_sub_den
added theorem Rat.sub_den_dvd
added theorem Rat.sub_den_dvd_lcm
added theorem Rat.sub_intCast_den
added theorem Rat.sub_natCast_den
added theorem Rat.sub_ofNat_den