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.