coe_C — Mathlib

English

The embedding preserves constant coefficients of C a: ((C a : R[X]) : PowerSeries R) = PowerSeries.C a.

Русский

Вложение сохраняет константный коэффициент C a: ((C a : R[X]) : PowerSeries R) = PowerSeries.C a.

LaTeX

$$$((C\\,a : R[X]) : PowerSeries R) = PowerSeries.C a$$$

Lean4

@[simp, norm_cast]
theorem coe_C (a : R) : ((C a : R[X]) : PowerSeries R) = PowerSeries.C a :=
  by
  have := coe_monomial 0 a
  rwa [PowerSeries.monomial_zero_eq_C_apply] at this

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