C_eq_algebraMap — Mathlib

English

For any r in R, the constant power series with value r equals its image under the canonical algebra map into power series: C r = (algebraMap R (PowerSeries R)) r.

Русский

Для любого r ∈ R константный ряд с коэффициентом r равен его образу под каноническим алгебраMap в степень-ряд: C r = (algebraMap R (PowerSeries R)) r.

LaTeX

$$$\\forall r:\\, R,\\ C r = (\\operatorname{algebraMap} R (PowerSeries R))\\, r$$$

Lean4

theorem C_eq_algebraMap {r : R} : C r = (algebraMap R R⟦X⟧) r :=
  rfl

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