isNat_rpow_neg — Mathlib

English

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

Русский

Если b = −nb и a^(−nb) целое, то a^b целое.

LaTeX

$$IsInt b (Int.negOfNat nb) → IsInt (a ^ (Int.negOfNat nb)) (Int.negOfNat ne) → IsInt (a ^ b) (Int.negOfNat ne)$$

Lean4

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

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