Theorems · Theorem · group theory

AddSubmonoid.LocalizationMap.neg_inj

∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {f : M →+ N}
  (hf : ∀ (y : ↥S), IsAddUnit (f ↑y)) {y z : ↥S},
  -(IsAddUnit.liftRight (f.domRestrict S) hf) y = -(IsAddUnit.liftRight (f.domRestrict S) hf) z → f ↑y = f ↑z

Given an AddMonoidHom f : M →+ N and Submonoid S ⊆ M such that f(S) ⊆ AddUnits N, for all y, z ∈ S, we have - (f y) = - (f z) → f y = f z.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

0 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidAddCommMonoid