coe_pow — Mathlib

English

Raising to a natural power and then coercing to rationals equals coercing first and then taking the power: (q^n) as a rational equals q^n.

Русский

Возведение в натуральную степень затем приведение к рациональным числам равно приведению к рациональным числам и взятию той же степени.

LaTeX

$$$$ \big(\uparrow(q^n)\big) : \mathbb{Q} = (q : \mathbb{Q})^n. $$$$

Lean4

@[simp, norm_cast]
theorem coe_pow (q : ℚ≥0) (n : ℕ) : (↑(q ^ n) : ℚ) = (q : ℚ) ^ n :=
  rfl

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