Commit 2024-05-09 09:01 e50d4102

View on Github →

feat(Rat, NNRat): q * q.den = q.num (#12739) and a few other lemmas. From LeanAPAP

Estimated changes

Modified Archive/Imo/Imo2013Q5.lean

Modified Mathlib/Data/NNRat/Defs.lean

added theorem NNRat.den_mul_eq_num

added theorem NNRat.divNat_mul_divNat

added theorem NNRat.divNat_mul_left

added theorem NNRat.divNat_mul_right

added theorem NNRat.divNat_zero

added theorem NNRat.mul_den_eq_num

added theorem NNRat.natCast_eq_divNat

Modified Mathlib/Data/Rat/Defs.lean

added theorem Rat.den_mul_eq_num

added theorem Rat.mul_den_eq_num

Modified Mathlib/Data/Rat/Lemmas.lean

deleted theorem Rat.mul_den_eq_num

Modified Mathlib/RingTheory/Localization/FractionRing.lean