Theorems · Definition · group theory

Submonoid.LocalizationMap.casesOn

{M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] →
          {motive : S.LocalizationMap N → Sort u} →
            (t : S.LocalizationMap N) →
              ((toMulHom : M →ₙ* N) →
                  (isLocalizationMap : S.IsLocalizationMap toMulHom.toFun) →
                    motive { toMulHom := toMulHom, isLocalizationMap := isLocalizationMap }) →
                motive t

Defined in

Mathlib.GroupTheory.MonoidLocalization.Basic

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

CommMonoidCommMonoid