zero — Mathlib

English

The substitution that sends every index to the zero power series is valid: HasSubst (fun _ => 0).

Русский

Замещение, отправляющее каждый индекс в нулевой ряд, допустимо: HasSubst (fun _ => 0).

LaTeX

$$HasSubst (fun (_ : σ) => (0 : MvPowerSeries τ S))$$

Lean4

theorem zero : HasSubst (fun (_ : σ) ↦ (0 : MvPowerSeries τ S)) :=
  by
  letI : UniformSpace S := ⊥
  simpa [hasSubst_iff_hasEval_of_discreteTopology] using HasEval.zero

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