Theorems · Theorem · ring theory

AddOreLocalization.vadd_oreSub

∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : VAddAssocClass R M X] (r : R) (x : X) (s : ↥S),
  r +ᵥ x -ₒ s = (AddOreLocalization.oreMin (r +ᵥ 0) s +ᵥ x) -ₒ AddOreLocalization.oreSubtra (r +ᵥ 0) s

Defined in

Mathlib.GroupTheory.OreLocalization.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddMonoidAddOreLocalization.AddOreSetAddActionVAddVAddVAddAssocClassVAddAssocClass