Commit 2024-01-05 00:28 86decee4

View on Github →

chore(Tactic/CancelDenoms/Core): slightly Qq-ify and golf (#9421) Using a stronger type for synthesizeUsingNormNum removes the need for a handful of lets.

Estimated changes

modified theorem CancelDenoms.derive_trans