differentiable_pow — Mathlib

English

For every natural n, the map x ↦ x^n is differentiable on the base algebra 𝔸.

Русский

Для каждого натурального n отображение x ↦ x^n дифференцируемо на алгебре 𝔸.

LaTeX

$$$\\forall n\\in\\mathbb{N},\\ \\text{Differentiable}_{\\mathbb{K}}(x\\mapsto x^{n})\\text{ on }\\mathbb{A}.$$$

Lean4

theorem differentiable_pow (n : ℕ) : Differentiable 𝕜 fun x : 𝔸 => x ^ n :=
  differentiable_id.pow _

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