mul_left — Mathlib

English

If HasSubst a holds, then multiplying on the left by any substitution b preserves HasSubst: HasSubst a → HasSubst b → HasSubst (b * a).

Русский

Если HasSubst a выполняется, умножение слева на любую подстановку b сохраняет HasSubst: HasSubst a → HasSubst b → HasSubst (b * a).

LaTeX

$$HasSubst a → HasSubst b → HasSubst (b * a)$$

Lean4

theorem mul_left (b : σ → MvPowerSeries τ S) {a : σ → MvPowerSeries τ S} (ha : HasSubst a) : HasSubst (b * a) :=
  by
  letI : UniformSpace S := ⊥
  rw [hasSubst_iff_hasEval_of_discreteTopology] at ha ⊢
  exact ha.mul_left b

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