comp_substAlgHom — Mathlib

English

The composition with ε equals aeval under the mapped ε: ε ∘ (substAlgHom ha) = aeval (ha.hasEval.map hε).

Русский

Составление с ε равно аeval, применённому к ha.hasEval.map hε: ε ∘ (substAlgHom ha) = aeval (ha.hasEval.map hε).

LaTeX

$$$\\varepsilon \\circ (\\operatorname{substAlgHom}(ha)) = \\operatorname{MvPowerSeries.aeval}(ha.hasEval.map h\\varepsilon)$$$

Lean4

theorem comp_substAlgHom [UniformSpace R] [DiscreteUniformity R] [UniformSpace S] [DiscreteUniformity S]
    (ha : HasSubst a) (hε : Continuous ε) : ε.comp (substAlgHom ha) = aeval (ha.hasEval.map hε) :=
  by
  ext f
  simp only [AlgHom.coe_comp, substAlgHom_eq_aeval ha]
  exact DFunLike.congr_fun (comp_aeval ha.hasEval hε) f

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