Theorem Rat.add_natCast_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.add_natCast_denView on Github →