Theorems · Theorem · group theory

Submonoid.LocalizationMap.mul_inv_right

∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
  (h : ∀ (y : ↥S), IsUnit (f ↑y)) (y : ↥S) (w z : N),
  z = w * ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ ↔ z * f ↑y = w

Given a MonoidHom f : M →* N and Submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all w, z : N and y ∈ S, we have z = w * (f y)⁻¹ ↔ z * f y = w.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoid