star'

Mathlib.Analysis.Calculus.Deriv.Star

URI: https://scilib.ai/kg/mathlib#deriv.star'

English

The derivative of the starred function equals the star of the derivative: deriv (star(f)) = star(deriv f).

Русский

Производная star(f) равна star(deriv f).

LaTeX

$$theorem deriv.star' : deriv (fun y => star (f y)) = fun x => star (deriv f x)$$

Lean4

@[simp]
protected theorem star' : (deriv fun y => star (f y)) = fun x => star (deriv f x) :=
  funext fun _ => deriv.star

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

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

Разделы

Аффилиация

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