OreLocalization.OreSet.ore_left_cancel
theorem OreLocalization.OreSet.ore_left_cancel :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [self : OreLocalization.OreSet S] (r₁ r₂ : R) (s : ↥S),
↑s * r₁ = ↑s * r₂ → ∃ s', r₁ * ↑s' = r₂ * ↑s'
This theorem, named `ore_left_cancel` from the `OreLocalization.OreSet` structure in Lean, asserts that in a monoid `R` with a designated submonoid `S`, if two elements `r₁` and `r₂` of `R` satisfy the equation `s * r₁ = s * r₂` for some `s` in `S` (where the multiplication is carried out in the monoid `R`), then there exists another element `s'` in `S` such that `r₁ * s' = r₂ * s'`. This is a weak form of cancellability, stating that common factors on the left can be turned into common factors on the right.
More concisely: In a monoid with a designated submonoid, if left multiplication by an element in the submonoid yields equal results for two elements, then there exists an element in the submonoid such that these elements are left multiples of each other.
|
OreLocalization.ore_eq
theorem OreLocalization.ore_eq :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r : R) (s : ↥S),
r * ↑(OreLocalization.oreDenom r s) = ↑s * OreLocalization.oreNum r s
The theorem `OreLocalization.ore_eq` states the Ore condition for a given fraction in an Ore localization. Specifically, for any type `R` endowed with a monoid structure, a submonoid `S` of `R`, and a pair of elements `(r, s)` where `r` is from `R` and `s` is from `S`, the product of `r` and the Ore denominator of the fraction `(r, s)` is equal to the product of `s` and the Ore numerator of the fraction `(r, s)`. This condition is crucial in the formation of Ore localizations in algebra, which are used to construct field of fractions in noncommutative settings.
More concisely: For any monoid `R` with submonoid `S`, and `r` in `R` and `s` in `S`, the Ore condition holds if and only if `r * OreDenominator (r, s) = OreNumerator (r, s) * s`.
|
OreLocalization.OreSet.ore_eq
theorem OreLocalization.OreSet.ore_eq :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [self : OreLocalization.OreSet S] (r : R) (s : ↥S),
r * ↑(OreLocalization.OreSet.oreDenom r s) = ↑s * OreLocalization.OreSet.oreNum r s
This theorem expresses the Ore condition for a fraction in the context of Ore localization. The Ore condition states that for any given type `R` that forms a monoid and submonoid `S` of `R`, along with an Ore localization of `S`, and given any element `r` of `R` and `s` from the submonoid `S`, the multiplication of `r` with the Ore denominator of the fraction `r/s` is equal to the multiplication of `s` with the Ore numerator of the fraction `r/s`. In mathematical terms, for any `r` in `R` and `s` in `S`, we have `r * oreDenom(r, s) = s * oreNum(r, s)`.
More concisely: For any ring `R` with monoid structure, submonoid `S`, and an Ore localization of `S`, the product of an element `r` in `R` with its Ore denominator equals the product of the Ore numerator with `s`, i.e., `r * oreDenom(r, s) = s * oreNum(r, s)`.
|
OreLocalization.ore_left_cancel
theorem OreLocalization.ore_left_cancel :
∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r₁ r₂ : R) (s : ↥S),
↑s * r₁ = ↑s * r₂ → ∃ s', r₁ * ↑s' = r₂ * ↑s'
This theorem, named `OreLocalization.ore_left_cancel`, states that in the context of a monoid `R` and a subset `S` of `R` that obeys the conditions of an Ore set, if two elements `r₁` and `r₂` of the monoid `R` satisfy the property that multiplying an element `s` from the set `S` with `r₁` equals multiplying the same element `s` with `r₂`, then there exists another element `s'` from the Ore set `S` such that the product of `r₁` and `s'` equals the product of `r₂` and `s'`. This essentially states a weak form of cancellability where common factors on the left of an equation can be swapped to the right.
More concisely: If `R` is a monoid with Ore set `S`, and `r₁r = r₂s` for some `r₁, r₂ in R` and `s in S`, then there exists `s' in S` such that `r₁s' = r₂s'`.
|