leibniz_div_const

Mathlib.RingTheory.Derivation.Basic

URI: https://scilib.ai/kg/mathlib#Derivation.leibniz_div_const

← MathLib Explorer

English

For a ∈ K and integer n, D(a^n) = n a^{n-1} D(a).

Русский

Для a ∈ K и целого n верно D(a^n) = n a^{n-1} D(a).

LaTeX

$$$D(a^{n}) = n \cdot a^{n-1} \cdot D(a)$ для всякого $a$ и целого $n$$$

Lean4

theorem leibniz_div_const (a b : K) (h : D b = 0) : D (a / b) = b⁻¹ • D a :=
  by
  simp only [leibniz_div, inv_pow, h, smul_zero, sub_zero, smul_smul]
  rw [← mul_self_mul_inv b⁻¹, inv_inv]
  ring_nf

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

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

Разделы

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

Аффилиация

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