Documentation

Mathlib.Algebra.DirectSum.AddChar

Direct sum of additive characters #

This file defines the direct sum of additive characters.

source
def AddChar.directSum {ι : Type u_1} {R : Type u_2} {G : ι → Type u_3} [DecidableEq ι] [(i : ι) → AddCommGroup (G i)] [CommMonoid R] (ψ : (i : ι) → AddChar (G i) R) :
AddChar (DirectSum ι fun (i : ι) => G i) R

Direct sum of additive characters.

Equations
Instances For
    source
    @[simp]
    theorem AddChar.directSum_apply {ι : Type u_1} {R : Type u_2} {G : ι → Type u_3} [DecidableEq ι] [(i : ι) → AddCommGroup (G i)] [CommMonoid R] (ψ : (i : ι) → AddChar (G i) R) (a✝ : DirectSum ι fun (i : ι) => G i) :
    (directSum ψ) a✝ = (DirectSum.toAddMonoid fun (i : ι) => toAddMonoidHomEquiv (ψ i)) a✝
    source
    theorem AddChar.directSum_injective {ι : Type u_1} {R : Type u_2} {G : ι → Type u_3} [DecidableEq ι] [(i : ι) → AddCommGroup (G i)] [CommMonoid R] :
    Function.Injective directSum