Theorems · Definition · group theory

DivisibleHull.liftOn

{M : Type u_1} →
  [inst : AddCommMonoid M] →
    {α : Type u_2} →
      DivisibleHull M →
        (f : M → ℕ+ → α) →
          (∀ (m m' : M) (s s' : ℕ+), DivisibleHull.mk m s = DivisibleHull.mk m' s' → f m s = f m' s') → α

If f : M → ℕ+ → α respects the equivalence on localization, lift it to a function DivisibleHull M → α.

Defined in

Mathlib.GroupTheory.DivisibleHull

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoid