Theorems · Theorem · group theory

Submonoid.LocalizationMap.AwayMap.lift_eq

∀ {M : Type u_1} [inst : CommMonoid M] {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3} [inst_2 : CommMonoid P]
  {g : M →* P} (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (hg : IsUnit (g x)) (a : M),
  (Submonoid.LocalizationMap.AwayMap.lift x F hg) (F a) = g a

Defined in

Mathlib.GroupTheory.MonoidLocalization.Away

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidCommMonoidCommMonoid