Theorems · Theorem · group theory

AddSubmonoid.LocalizationMap.add_neg

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

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

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoid