Theorems · Definition · ring theory

OreLocalization.liftExpand

{R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_3} →
          [inst_2 : MulAction R X] →
            {C : Sort u_2} →
              (P : X → ↥S → C) →
                (∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩) → OreLocalization S X → C

A function or predicate over X and S can be lifted to X[S⁻¹] if it is invariant under expansion on the left.

Defined in

Mathlib.GroupTheory.OreLocalization.Basic

Cited by

1 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext

Assumes

MonoidOreLocalization.OreSetMulAction