mk_zpow — Mathlib

English

Powers inside the nonnegative subtype correspond to powers in α: (⟨x, hx⟩)^n = ⟨x^n, zpow_nonneg hx n⟩.

Русский

Степени внутри неотрицательного подмножества соответствуют степеням в α: (⟨x, hx⟩)^n = ⟨x^n, zpow_nonneg hx n⟩.

LaTeX

$$$ (\\langle x, hx \\rangle)^n = \\langle x^n, zpow\\_nonneg hx n \\rangle $$$

Lean4

@[simp]
theorem mk_zpow (hx : 0 ≤ x) (n : ℤ) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) ^ n = ⟨x ^ n, zpow_nonneg hx n⟩ :=
  rfl

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