Theorem Rat.num_mk

Modification history

2025-12-27 09:41
Mathlib/Data/Rat/Lemmas.lean
chore(Data/Rat/Lemmas): deprecate `num_mk` and `den_mk` (#33334)
Modified Rat.num_mkView on Github →
2025-05-07 11:29
Mathlib/Data/Rat/Lemmas.lean
chore: adaptations for batteries#1225 (#24625)
Added Rat.num_mkView on Github →
2025-05-05 23:17
Mathlib/Data/Rat/Lemmas.lean
chore: bump toolchain to v4.20.0-rc3 (#24621)
Deleted Rat.num_mkView on Github →
2022-12-24 07:34
Mathlib/Data/Rat/Lemmas.lean
feat: port Data.Rat.Lemmas (#1138)
Added Rat.num_mkView on Github →