Theorems · Theorem · ring theory

AddOreLocalization.oreSub_vadd_char

∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ : ↥S) (r' : R) (s' : ↥S),
  ↑s' + r₁ = r' + ↑s₂ → (r₁ -ₒ s₁) +ᵥ r₂ -ₒ s₂ = (r' +ᵥ r₂) -ₒ (s' + s₁)

A characterization lemma for the vector addition on the Ore localization, allowing for a choice of Ore minuend and Ore subtrahend.

Defined in

Mathlib.GroupTheory.OreLocalization.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddMonoidAddOreLocalization.AddOreSetAddAction