Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-08 07:55 c360e01a

View on Github →

feat(ring/localization): add fraction map for int to rat cast (#2921)

Estimated changes

Modified src/data/rat/basic.lean

added theorem rat.mul_denom_eq_num

deleted theorem rat.mul_own_denom_eq_num

Modified src/ring_theory/localization.lean

added def fraction_map.int.fraction_map