Theorems · Theorem · ring theory

DirectSum.algebraMap_apply

∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) [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 : DirectSum.GAlgebra R A] [inst_6 : DecidableEq ι] (r : R),
  (algebraMap R (DirectSum ι fun i => A i)) r = (DirectSum.of A 0) (DirectSum.GAlgebra.toFun r)

Defined in

Mathlib.Algebra.DirectSum.Algebra

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddMonoidDirectSum.GSemiringDirectSum.GAlgebraDecidableEq