dpow — Mathlib

English

In a rational algebra setting, the divided power structure is given by dpow n x = x^n / n! and is compatible with ℚ-structures on I.

Русский

В рамках рациональных алгебр структура разделённых степеней задаётся dpow n x = x^n / n! и совместима с ℚ-структурами на I.

LaTeX

$$$dpow\_I(n, x) = x^n / n! \quad (\text{for } x \in I)$$$

Lean4

/-- The family `ℕ → R → R` given by `dpow n x = x ^ n / n!`. -/
noncomputable def dpow : ℕ → R → R :=
  OfInvertibleFactorial.dpow I

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