npow

Mathlib.GroupTheory.OreLocalization.Basic

URI: https://scilib.ai/kg/mathlib#OreLocalization.npow

← MathLib Explorer

English

`npow` defines natural-number power on the Ore localization.

Русский

`npow` задаёт естественную степень на локализации Оре.

LaTeX

$$$ \text{npow} : \mathbb{N} \to (R[S^{-1}] \to R[S^{-1}]), \ n \mapsto x^n $$$

Lean4

/-- `npow` of `OreLocalization` -/
@[to_additive (attr := irreducible) /-- `nsmul` of `AddOreLocalization` -/
    ]
protected def npow : ℕ → R[S⁻¹] → R[S⁻¹] :=
  npowRec

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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