Theorems · Theorem · group theory

Submonoid.LocalizationMap.mul_inv_left

∀ {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),
  w * ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ = z ↔ w = f ↑y * z

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 w * (f y)⁻¹ = z ↔ w = f y * z.

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

15 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoid