Commit 2025-12-27 09:41 a39c234f

View on Github →

chore(Data/Rat/Lemmas): deprecate num_mk and den_mk (#33334)

Estimated changes

modified theorem Rat.den_mk
modified theorem Rat.num_mk