Theorem Rat.natCast_add_den

Modification history

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