Commit 2024-02-03 14:26 b2f2f2cf

View on Github →

feat: num and den lemmas (#10219) Add a few basic lemmas about Rat and NNRat and fix some lemma names From LeanAPAP

Estimated changes

deleted theorem Rat.coe_nat_den
deleted theorem Rat.coe_nat_num
added theorem Rat.den_natCast
added theorem Rat.den_ofNat
added theorem Rat.num_natCast
added theorem Rat.num_ofNat
modified def NNRat.den
modified theorem NNRat.den_coe
added theorem NNRat.den_natCast
added theorem NNRat.den_pos
modified theorem NNRat.natAbs_num_coe
modified def NNRat.num
added theorem NNRat.num_coe
added theorem NNRat.num_natCast
added theorem NNRat.num_ne_zero
added theorem NNRat.num_pos