Theorems · Theorem · group theory

AddChar.coe_mk

∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (f : A → M) (map_zero_eq_one' : f 0 = 1)
  (map_add_eq_mul' : ∀ (a b : A), f (a + b) = f a * f b),
  ⇑{ toFun := f, map_zero_eq_one' := map_zero_eq_one', map_add_eq_mul' := map_add_eq_mul' } = f

Defined in

Mathlib.Algebra.Group.AddChar

Cited by

5 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

AddMonoidMonoid