English
Under differentiability of c and d within s at x, the derivative within s of the product c d equals the sum of two products as in the product rule.
Русский
При дифференцируемости внутри s функций c и d, производная внутри s от произведения равна сумме двух произведений по правилу произведения.
LaTeX
$$$\operatorname{derivWithin}(c \cdot d) \, s \, x = (\operatorname{derivWithin} c \, s \, x) \cdot d(x) + c(x) \cdot (\operatorname{derivWithin} d \, s \, x)$$$
Lean4
theorem deriv_mul_const_field (v : 𝕜') : deriv (fun y => u y * v) x = deriv u x * v :=
by
by_cases hu : DifferentiableAt 𝕜 u x
· exact deriv_mul_const hu v
· rw [deriv_zero_of_not_differentiableAt hu, zero_mul]
rcases eq_or_ne v 0 with (rfl | hd)
· simp only [mul_zero, deriv_const]
· refine deriv_zero_of_not_differentiableAt (mt (fun H => ?_) hu)
simpa only [mul_inv_cancel_right₀ hd] using H.mul_const v⁻¹
