mapCoeffs_C

Mathlib.RingTheory.Derivation.MapCoeffs

URI: https://scilib.ai/kg/mathlib#Differential.mapCoeffs_C

English

For constant C(x), mapCoeffs(C(x)) yields the constant coefficient vector with d(x) at degree 0.

Русский

Для константы C(x) mapCoeffs(C(x)) даёт коэффициент нулевой степени равный d(x).

LaTeX

$$$\mathrm{mapCoeffs}(\mathrm{C}(x)) = \mathrm{single}^{A}_{0}(d(x)).$$$

Lean4

@[simp]
theorem mapCoeffs_C (x : A) : mapCoeffs (C x) = C x′ := by simp [← monomial_zero_left]

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

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

Разделы

Аффилиация

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