Theorems · Theorem · ring theory

OreLocalization.liftExpand_of

∀ {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}
  {hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩} (r : X) (s : ↥S),
  OreLocalization.liftExpand P hP (r /ₒ s) = P r s

Defined in

Mathlib.GroupTheory.OreLocalization.Basic

Cited by

0 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext

Assumes

MonoidOreLocalization.OreSetMulAction