Theorems · Definition · group theory

DirectSum.setToSet

{ι : Type v} →
  (β : ι → Type w) →
    [inst : (i : ι) → AddCommMonoid (β i)] →
      [DecidableEq ι] → (S T : Set ι) → S ⊆ T → (DirectSum ↑S fun i => β ↑i) →+ DirectSum ↑T fun i => β ↑i

setToSet β S T h is the natural homomorphism ⨁ (i : S), β i → ⨁ (i : T), β i, where h : S ⊆ T.

Defined in

Mathlib.Algebra.DirectSum.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidableEq