algHom_ext — Mathlib

English

If two algebra homomorphisms f,g from the direct sum to B agree on each inclusion of A i, then f = g.

Русский

Если два алгебраических гомоморфизма f,g от прямой суммы к B совпадают на каждом включении A i, тогда f = g.

LaTeX

$$∀ {f,g : (⊕ i, A i) →ₐ[R] B}, (∀ i x, f(of A i x) = g(of A i x)) ⇒ f = g$$

Lean4

theorem algHom_ext ⦃f g : (⨁ i, A i) →ₐ[R] B⦄ (h : ∀ i x, f (of A i x) = g (of A i x)) : f = g :=
  algHom_ext' R A fun i => LinearMap.ext <| h i

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