isInt_rpow_neg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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