cast_pow — Mathlib

English

For p ∈ ℚ and n ∈ ℕ, the cast of p^n equals (p^n) in α.

Русский

Для p ∈ ℚ и n ∈ ℕ приводение p^n в α равно p^n в α.

LaTeX

$$$\forall p \in \mathbb{Q}, \forall n \in \mathbb{N},\ ↑(p^n) = (p^n : \alpha).$$$

Lean4

@[simp, norm_cast]
theorem cast_pow (p : ℚ) (n : ℕ) : ↑(p ^ n) = (p ^ n : α) := by
  rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow, ←
    (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]

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