Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-08-24 17:49
1f5ee2b5
View on Github →
feat(Rat/Lemmas): add lemmas about
(q ± n).den
(
#28809
)
Estimated changes
Modified
Mathlib/Data/Rat/Lemmas.lean
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