Theorems · Theorem · ring theory

OreLocalization.oreDiv_smul_oreDiv

∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] {r₁ : R} {r₂ : X} {s₁ s₂ : ↥S},
  (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = OreLocalization.oreNum r₁ s₂ • r₂ /ₒ (OreLocalization.oreDenom r₁ s₂ * s₁)

Defined in

Mathlib.GroupTheory.OreLocalization.Basic

Cited by

3 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Quot.sound

Assumes

MonoidOreLocalization.OreSetMulAction