Theorems · Theorem · ring theory

OreLocalization.add_oreDiv

∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] {r r' : X} {s : ↥S}, r /ₒ s + r' /ₒ s = (r + r') /ₒ s

Defined in

Mathlib.RingTheory.OreLocalization.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

MonoidOreLocalization.OreSetAddMonoidDistribMulAction