Theorems · Inductive type · group theory

AddChar

(A : Type u_1) → [AddMonoid A] → (M : Type u_2) → [Monoid M] → Type (max u_1 u_2)

AddChar A M is the type of maps A → M, for A an additive monoid and M a multiplicative monoid, which intertwine addition in A with multiplication in M. We only put the typeclasses needed for the definition, although in practice we are usually interested in much more specific cases (e.g. when A is a group and M a commutative ring).

Defined in

Mathlib.Algebra.Group.AddChar

Cited by

286 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

AddMonoidMonoid