Commit 2024-04-30 10:36 37351aa9
View on Github →feat(Rat): Numerator and denominator of q ^ n
(#12506)
Prove (q ^ n).num = q.num ^ n
and (q ^ n).den = q.den ^ n
by making those defeq. It is somewhat painful. (q ^ n).den = q.den ^ n
is also defeq for NNRat
, but not (q ^ n).num = q.num ^ n
due to the Int.natAbs
in the definition of NNRat.num
.