coe_pow — Mathlib

English

Let a ∈ α and n ∈ ℕ. The power a^n, when viewed in WithTop α via the natural embedding, equals the image of a^n in α under the same embedding.

Русский

Пусть a ∈ α и n ∈ ℕ. Степень a^n, рассматриваемая внутри WithTop α через естественное вложение, равна образу a^n в α под тем же вложением.

LaTeX

$$$ (↑(a^n) : \\mathrm{WithTop} \\alpha) = a^n $$$

Lean4

@[simp, norm_cast]
theorem coe_pow (a : α) (n : ℕ) : (↑(a ^ n) : WithTop α) = a ^ n :=
  rfl

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