coe_pow — Mathlib

English

Let a ∈ SignType and k ∈ ℕ. The natural embedding SignType → α preserves nth powers: ↑(a^k) = (a:α)^k.

Русский

Пусть a ∈ SignType и k ∈ ℕ. Вложение SignType → α сохраняет возведение в степень: ↑(a^k) = (a : α)^k.

LaTeX

$$$\uparrow(a^k) = (a : \alpha)^k$$$

Lean4

@[simp, norm_cast]
theorem coe_pow {α} [MonoidWithZero α] [HasDistribNeg α] (a : SignType) (k : ℕ) : ↑(a ^ k) = (a : α) ^ k :=
  map_pow SignType.castHom _ _

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