Theorems · Theorem · ring theory

DirectSum.algHom_ext

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

Defined in

Mathlib.Algebra.DirectSum.Algebra

Cited by

0 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleAddMonoidDirectSum.GSemiringSemiringDirectSum.GAlgebraAlgebraDecidableEq