Theorems · Theorem · ring theory

OreLocalization.add_smul

∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddCommMonoid X] [inst_3 : Module R X] (y z : OreLocalization S R) (x : OreLocalization S X),
  (y + z) • x = y • x + z • x

Defined in

Mathlib.RingTheory.OreLocalization.Ring

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringOreLocalization.OreSetAddCommMonoidModule