coe_pow

Mathlib.Algebra.Order.Nonneg.Basic

URI: https://scilib.ai/kg/mathlib#Nonneg.coe_pow

English

Coercion commutes with exponentiation: the underlying power equals the power of the underlying.

Русский

Коммутативность приведения с возведением в степень: основанная степень равна степени основания.

LaTeX

$$$ (a^n : \alpha) = (a : \alpha)^n $$$

Lean4

@[simp, norm_cast]
protected theorem coe_pow (a : { x : α // 0 ≤ x }) (n : ℕ) : (↑(a ^ n) : α) = (a : α) ^ n :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru