lineDeriv

Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap

URI: https://scilib.ai/kg/mathlib#QuadraticMap.lineDeriv

English

For any quadratic map f, the line derivative equals the polar form.

Русский

Для любого квадратичного отображения f линейная производная равна полярной форме.

LaTeX

$$$ lineDeriv 𝕜 f = polar f $$$

Lean4

@[simp]
protected theorem lineDeriv (f : QuadraticMap 𝕜 E F) : lineDeriv 𝕜 f = polar f :=
  by
  ext a b
  exact (f.hasLineDerivAt a b).lineDeriv

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

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

Разделы

Аффилиация

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