logDeriv_pow — Mathlib

English

Let R be a field equipped with a differential structure. Then for any natural number n and any a in R, the logarithmic derivative satisfies logDeriv(a^n) = n · logDeriv(a).

Русский

Пусть R — поле с дифференциалом. Для любого натурального числа n и элемента a ∈ R выполняется logDeriv(a^n) = n · logDeriv(a).

LaTeX

$$$\\logDeriv(a^n) = n\\,\\logDeriv(a)$$$

Lean4

@[simp]
theorem logDeriv_pow (n : ℕ) (a : R) : logDeriv (a ^ n) = n * logDeriv a := by
  induction n with
  | zero => simp
  | succ n h2 =>
    obtain rfl | hb := eq_or_ne a 0
    · simp
    · rw [Nat.cast_add, Nat.cast_one, add_mul, one_mul, ← h2, pow_succ, logDeriv_mul] <;> simp [hb]

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