coe_one — Mathlib

English

The constant polynomial 1, viewed as a power series, is the unit 1 in PowerSeries R: ((1 : R[X]) : PowerSeries R) = 1.

Русский

Единичный константный полином, трактуемый как ряд, является единицей: ((1 : R[X]) : PowerSeries R) = 1.

LaTeX

$$$((1 : R[X]) : PowerSeries R) = 1$$$

Lean4

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

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