subst_self — Mathlib

English

Substituting the variable X by itself yields the identity map: subst(X) = id.

Русский

Подстановка по переменной X возвращает тождественное отображение: subst(X) = id.

LaTeX

$$$\\operatorname{subst}(\\mathrm{X}) = \\mathrm{id}$.$$

Lean4

theorem subst_self : subst (MvPowerSeries.X : σ → MvPowerSeries σ R) = id :=
  by
  rw [← coe_substAlgHom HasSubst.X]
  letI : UniformSpace R := ⊥
  ext1 f
  simp only [substAlgHom_eq_aeval]
  have := aeval_unique (ε := AlgHom.id R (MvPowerSeries σ R)) continuous_id
  rw [DFunLike.ext_iff] at this
  exact this f

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