Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-03-14 03:22
70662e1c
View on Github →
chore(data/rat/basic): a few trivial lemmas about
rat.denom
(
#6667
)
Estimated changes
Modified
src/data/rat/basic.lean
added
theorem
rat.add_denom_dvd
modified
theorem
rat.denom_neg_eq_denom
added
theorem
rat.denom_zero
added
theorem
rat.mk_pnat_denom_dvd
added
theorem
rat.mul_denom_dvd
modified
theorem
rat.num_neg_eq_neg_num
Modified
src/data/rat/order.lean