English
For q ∈ ℚ≥0 and n ∈ ℕ, NNRat.cast (q^n) = (NNRat.cast q : K)^n for any DivisionSemiring K.
Русский
Для q ∈ ℚ≥0 и n ∈ ℕ выполняется NNRat.cast (q^n) = (NNRat.cast q : K)^n для любого кольца с делением K.
LaTeX
$$$ \forall K [DivisionSemiring K] (q : \mathbb{Q}_{\ge 0}) (n : \mathbb{N}), \, NNRat.cast (q ^ n) = (NNRat.cast q : K) ^ n. $$$
Lean4
@[simp, norm_cast]
theorem cast_pow {K} [DivisionSemiring K] (q : ℚ≥0) (n : ℕ) : NNRat.cast (q ^ n) = (NNRat.cast q : K) ^ n := by
rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow, ←
(Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
