dpow — Mathlib

English

In the setting of an ideal I and a DecidablePred membership, the dpow_n is defined by x^n/n! if x ∈ I, and is 0 otherwise; this is formalized in DividedPowers.OfInvertibleFactorial.

Русский

Для dpow_n применяется x^n/n! если x ∈ I, иначе 0; определение через факториал, когда I допускает инверсию, формализовано в DividedPowers.OfInvertibleFactorial.

LaTeX

$$$dpow\\ I\\; n\\; x = \\begin{cases} inverse(n! ) \\cdot x^n, & x \\in I \\\\ 0, & x \\notin I \\end{cases}$$$

Lean4

/-- The family of functions `ℕ → A → A` given by `x^n/n!`. -/
noncomputable def dpow : ℕ → A → A := fun m x => if x ∈ I then inverse (m ! : A) * x ^ m else 0

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