C — Mathlib · SciLib

English

There is a canonical inclusion of R into MvPowerSeries σ R given by sending a to the constant series with value a.

Русский

Существует каноническое вложение R в MvPowerSeries σ R, отправляющее a в константный ряд со значением a.

LaTeX

$$$$ C : R \to^+_* MvPowerSeries(σ,R) $$$$

Lean4

/-- The constant multivariate formal power series. -/
def C : R →+* MvPowerSeries σ R :=
  { monomial (0 : σ →₀ ℕ) with
    map_one' := rfl
    map_mul' := fun a b => Eq.trans (by simp) (monomial_mul_monomial _ _ a b).symm
    map_zero' := (monomial 0).map_zero }

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