Documentation

Mathlib.Algebra.DirectSum.AddChar

Direct sum of additive characters #

This file defines the direct sum of additive characters.

@[simp]
theorem AddChar.directSum_toFun {ι : 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), (AddChar.directSum ψ) a = (DirectSum.toAddMonoid fun (i : ι) => AddChar.toAddMonoidHomEquiv (ψ i)) a
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
    theorem AddChar.directSum_injective {ι : Type u_1} {R : Type u_2} {G : ιType u_3} [DecidableEq ι] [(i : ι) → AddCommGroup (G i)] [CommMonoid R] :
    Function.Injective AddChar.directSum