Theorem Rat.sub_den_dvd_lcm

Modification history

2025-08-24 17:49
Mathlib/Data/Rat/Lemmas.lean
feat(Rat/Lemmas): add lemmas about `(q ± n).den` (#28809)
Added Rat.sub_den_dvd_lcmView on Github →