coe_zero — Mathlib

English

The constant Laurent series corresponding to 1 is the embedding of 1 from R into LaurentSeries: ((1 : PowerSeries R) : LaurentSeries R) = 1.

Русский

Единица из R в Лаурентовых рядах конвертируется в единицу как константный ряд: (1 : PowerSeries R) в LaurentSeries R равна 1.

LaTeX

$$$((1 : R)\,\text{in PowerSeries } R) : R⟨X⟩ = 1$$$

Lean4

@[norm_cast]
theorem coe_zero : ((0 : R⟦X⟧) : R⸨X⸩) = 0 :=
  (ofPowerSeries ℤ R).map_zero

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