algHom_ext' — Mathlib

English

Applying lift to an element of R via inl yields f r.

Русский

Применение lift к элементу r через inl даёт f r.

LaTeX

$$$ lift(f,g,hg,hfg,hgf)(inl\\, r) = f(r) $$$

Lean4

@[ext]
theorem algHom_ext' {A} [Semiring A] [Algebra S A] ⦃f g : tsze R M →ₐ[S] A⦄
    (hinl : f.comp (inlAlgHom S R M) = g.comp (inlAlgHom S R M))
    (hinr :
      f.toLinearMap.comp (inrHom R M |>.restrictScalars S) = g.toLinearMap.comp (inrHom R M |>.restrictScalars S)) :
    f = g :=
  AlgHom.toLinearMap_injective <| linearMap_ext (AlgHom.congr_fun hinl) (LinearMap.congr_fun hinr)

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