English
The derivative of f(c x) with respect to x is c times the derivative of f at the point c x.
Русский
Производная функции f(c x) по x равна c умноженному на производную f в точке c x.
LaTeX
$$$$deriv\ (fun x => f( c \cdot x ))\ x = c \cdot deriv\ f (c \cdot x)$$$$
Lean4
theorem hasStrictDerivAt_inv (hx : x ≠ 0) : HasStrictDerivAt Inv.inv (-(x ^ 2)⁻¹) x :=
by
suffices (fun p : 𝕜 × 𝕜 => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p => (p.1 - p.2) * 1
by
refine .of_isLittleO <| this.congr' ?_ (Eventually.of_forall fun _ => mul_one _)
refine Eventually.mono ((isOpen_ne.prod isOpen_ne).mem_nhds ⟨hx, hx⟩) ?_
rintro ⟨y, z⟩ ⟨hy, hz⟩
simp only [mem_setOf_eq] at hy hz
simp [field]
ring
refine (isBigO_refl (fun p : 𝕜 × 𝕜 => p.1 - p.2) _).mul_isLittleO ((isLittleO_one_iff 𝕜).2 ?_)
rw [← sub_self (x * x)⁻¹]
exact tendsto_const_nhds.sub ((continuous_mul.tendsto (x, x)).inv₀ <| mul_ne_zero hx hx)
