Theorem Rat.den_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.den_mk View on Github →

2022-12-24 07:34

Mathlib/Data/Rat/Lemmas.lean

feat: port Data.Rat.Lemmas (#1138)

Added Rat.den_mk View on Github →