DirectSum.algHom_ext'

theorem DirectSum.algHom_ext' : ∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [inst : DecidableEq ι] [inst_1 : CommSemiring R] [inst_2 : (i : ι) → AddCommMonoid (A i)] [inst_3 : (i : ι) → Module R (A i)] [inst_4 : AddMonoid ι] [inst_5 : DirectSum.GSemiring A] [inst_6 : Semiring B] [inst_7 : DirectSum.GAlgebra R A] [inst_8 : Algebra R B] ⦃f g : (DirectSum ι fun i => A i) →ₐ[R] B⦄, (∀ (i : ι), f.toLinearMap ∘ₗ DirectSum.lof R ι A i = g.toLinearMap ∘ₗ DirectSum.lof R ι A i) → f = g

The theorem `DirectSum.algHom_ext'` states that for any type `ι`, any commutative semiring `R`, a family of types `A : ι → Type`, and a type `B`, given decidable equality on `ι`, the fact that `A i` is an additive commutative monoid and a module over `R` for each `i : ι`, an additive monoid structure on `ι`, a graded semiring structure on `A`, a semiring structure on `B`, a graded algebra structure from `R` to `A`, and an algebra structure from `R` to `B`, if we have two algebra homomorphisms `f` and `g` from the direct sum of `A i` over `ι` to `B`, and for each `i : ι`, the composition of `f.toLinearMap` and the linear map from `A i` to the direct sum given by `DirectSum.lof` is equal to the composition of `g.toLinearMap` and the same linear map, then `f` and `g` are equal. In simpler terms, two algebra homomorphisms from a direct sum to another algebra are equal if they agree on all components of the direct sum.

More concisely: Given commutative semirings R, types A i (i : ι) and B, decidable equality on ι, and given that A i is an additive commutative monoid and an R-module, A has a graded semiring and R-algebra structures, and B has a semiring structure; if f and g are algebra homomorphisms from the direct sum of A i to B such that the composition of each homomorphism with the linear map from A i to the direct sum is equal, then f and g are equal.