coe_mul

Mathlib.RingTheory.LaurentSeries

URI: https://scilib.ai/kg/mathlib#PowerSeries.coe_mul

English

The coercion respects multiplication: ((f * g : PowerSeries R) : LaurentSeries R) = f * g.

Русский

Отображение сохраняет умножение: ((f * g : PowerSeries R) : LaurentSeries R) = f * g.

LaTeX

$$$((f * g : PowerSeries R) : LaurentSeries R) = f * g$$$

Lean4

@[norm_cast]
theorem coe_mul : ((f * g : R⟦X⟧) : R⸨X⸩) = f * g :=
  (ofPowerSeries ℤ R).map_mul _ _

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

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

Разделы

Аффилиация

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