uzpow_coe_nat

Mathlib.Data.ZMod.IntUnitsPower

URI: https://scilib.ai/kg/mathlib#uzpow_coe_nat

English

Uzpow respects coercions from Nat to R on UnitsInt; (s : Units Int)^(n: R) equals s^(n).

Русский

Uzpow сохраняет приведённые к R неотрицательные степени для Units Int: s^(n: R) = s^n.

LaTeX

$$$s^{(n: R)} = s^{n}$ for s : \mathbb{Z}^{\times}, n \in \mathbb{N}.$$$

Lean4

theorem uzpow_coe_nat (s : ℤˣ) (n : ℕ) [n.AtLeastTwo] : s ^ (ofNat(n) : R) = s ^ (ofNat(n) : ℕ) :=
  uzpow_natCast _ _

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

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

Разделы

Аффилиация

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