Theorems · Theorem · ring theory

OreLocalization.ind

∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] {β : OreLocalization S X → Prop},
  (∀ (r : X) (s : ↥S), β (r /ₒ s)) → ∀ (q : OreLocalization S X), β q

Defined in

Mathlib.GroupTheory.OreLocalization.Basic

Cited by

18 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext

Assumes

MonoidOreLocalization.OreSetMulAction