derivation_C

Mathlib.Algebra.Polynomial.Derivation

URI: https://scilib.ai/kg/mathlib#Polynomial.derivation_C

English

For all a ∈ A and f ∈ R[X], mkDerivation R a f equals the derivative of f multiplied by a.

Русский

Для всех a ∈ A и f ∈ R[X], mkDerivation R a f совпадает с производной f, умноженной на a.

LaTeX

$$$mkDerivation\ R\ a\ f = (\mathrm{derivative}\; f) \cdot a$$$

Lean4

@[simp]
theorem derivation_C (D : Derivation R R[X] A) (a : R) : D (C a) = 0 :=
  D.map_algebraMap a

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

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

Разделы

Аффилиация

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