cast_zpow_of_ne_zero — Mathlib

English

If z ∈ ℤ and q ∈ ℚ≥0 with q.num ≠ 0 in K, then NNRat.cast (q^z) = (NNRat.cast q : K)^z.

Русский

Если z ∈ ℤ и q ∈ ℚ≥0 с q.num ≠ 0 в K, то NNRat.cast (q^z) = (NNRat.cast q : K)^z.

LaTeX

$$$ ∀ K [DivisionSemiring K] (q : \mathbb{Q}_{\ge 0}) (z : \mathbb{Z}), q.num.cast \neq 0 → NNRat.cast (q ^ z) = (NNRat.cast q : K) ^ z. $$$

Lean4

theorem cast_zpow_of_ne_zero {K} [DivisionSemiring K] (q : ℚ≥0) (z : ℤ) (hq : (q.num : K) ≠ 0) :
    NNRat.cast (q ^ z) = (NNRat.cast q : K) ^ z :=
  by
  obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
  · simp
  · simp_rw [zpow_neg, zpow_natCast, ← inv_pow, NNRat.cast_pow]
    congr
    rw [cast_inv_of_ne_zero hq]

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