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.

Estimated changes

added theorem Rat.den_pow
added theorem Rat.divInt_pow
modified theorem Rat.intCast_div_eq_divInt
added theorem Rat.mk'_mul_mk'
added theorem Rat.mk'_num_den
added theorem Rat.mk'_pow
added theorem Rat.mkRat_pow
added theorem Rat.num_pow
added theorem Rat.pow_def
added theorem Rat.pow_eq_divInt
added theorem Rat.pow_eq_mkRat