Theorems · Definition · group theory

AddChar.toAddMonoidHomEquiv

{A : Type u_1} → {M : Type u_3} → [inst : AddMonoid A] → [inst_1 : Monoid M] → AddChar A M ≃ (A →+ Additive M)

Additive characters A → M are the same thing as additive homomorphisms from A to Additive M.

Defined in

Mathlib.Algebra.Group.AddChar

Cited by

8 results in Mathlib

Foundations

Depth 18 from the axioms · uses Quot.sound

Assumes

AddMonoidMonoid