coe_pow — Mathlib

English

For a ∈ α and n ∈ ℕ, the embedding of a^n into WithBot α equals a^n in WithBot α. The embedding preserves exponentiation.

Русский

Для a ∈ α и n ∈ ℕ вложение a^n в WithBot α совпадает с a^n в WithBot α; возведение в степень сохраняется под вложением.

LaTeX

$$$ (↑(a^n) : WithBot α) = a^n $$$

Lean4

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

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