algHom_ext — Mathlib

English

Two R-algebra morphisms from R[ε] to A are equal if they agree on ε.

Русский

Два R-алгебра-гомоморфизмa из R[ε] в A равны, если они согласны на ε.

LaTeX

$$$\text{If } f,g: R[ε] \to A \text{ are } R\text{-algebra morphisms, and } f(ε) = g(ε), \text{ then } f = g$$$

Lean4

/-- For two `R`-algebra morphisms out of `R[ε]` to agree, it suffices for them to agree on `ε`. -/
@[ext 1200]
theorem algHom_ext ⦃f g : R[ε] →ₐ[R] A⦄ (hε : f ε = g ε) : f = g :=
  by
  ext
  dsimp
  simp only [one_smul, hε]

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