pow_right — Mathlib

English

For all a ∈ ℤ and b,e ∈ ℕ, J(a | b^e) = J(a | b)^e.

Русский

Пусть a ∈ ℤ и b,e ∈ ℕ. Тогда J(a | b^e) = J(a | b)^e.

LaTeX

$$$ J(a | b^e) = J(a | b)^e $$$

Lean4

/-- We have that `J(a | b^e) = J(a | b)^e`. -/
theorem pow_right (a : ℤ) (b e : ℕ) : J(a | b ^ e) = J(a | b) ^ e := by
  induction e with
  | zero => rw [Nat.pow_zero, _root_.pow_zero, one_right]
  | succ e ih =>
    rcases eq_zero_or_neZero b with hb | _
    · rw [hb, zero_pow e.succ_ne_zero, zero_right, one_pow]
    · rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]

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