Theorems · Theorem · group theory

AddUnits.map_mk

∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N) (val neg : M)
  (val_neg : val + neg = 0) (neg_val : neg + val = 0),
  (AddUnits.map f) { val := val, neg := neg, val_neg := val_neg, neg_val := neg_val } =
    { val := f val, neg := f neg, val_neg := ⋯, neg_val := ⋯ }

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext

Assumes

AddMonoidAddMonoid