isNNRat_rpow_neg — Mathlib

English

If b is an integer −nb and a^(−nb) is a nonnegative rational, then a^b is a nonnegative rational.

Русский

Если b = −nb целое и a^(−nb) — неотрицательная рациональная дробь, то a^b — неотрицательная рациональная дробь.

LaTeX

$$IsInt b (Int.negOfNat nb) → IsNNRat (a ^ (Int.negOfNat nb)) num den → IsNNRat (a ^ b) num den$$

Lean4

theorem isNNRat_rpow_neg {a b : ℝ} {nb : ℕ} {num den : ℕ} (pb : IsInt b (Int.negOfNat nb))
    (pe' : IsNNRat (a ^ (Int.negOfNat nb)) num den) : IsNNRat (a ^ b) num den := by rwa [pb.out, Real.rpow_intCast]

Похожие утверждения