ofAdd_zpow — Mathlib

English

Relates the image of an integer under the additive embedding to the corresponding exponentiation in the zero-augmented integers; a compatibility between additive and multiplicative viewpoints.

Русский

Устанавливает связь между отображением целого числа через аддитивное вложение и соответствующим возведением в степень в нулевой аугментации; совместимость аддитивного и умножения.

LaTeX

$$$\\bigl( \\uparrow(\\operatorname{ofAdd}(a)) : \\mathbb{Z}^{0} \\bigr) = \\operatorname{ofAdd}(1)^{a}$$$

Lean4

@[deprecated exp_zsmul (since := "2025-05-17")]
theorem ofAdd_zpow (a : ℤ) : (↑(ofAdd a) : ℤᵐ⁰) = ofAdd (1 : ℤ) ^ a :=
  show exp a = exp 1 ^ a by simp

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