nonempty_oreSet_iff_of_noZeroDivisors

English

In a NoZeroDivisors ring, Nonempty(OreSet S) iff ∀ r ∈ R, s ∈ S ∃ r', s' ∈ S with s' r = r' s.

Русский

В кольце без нулевых делителей Nonempty(OreSet S) эквивалентно ∀ r ∈ R, s ∈ S, ∃ r', s' ∈ S, s' r = r' s.

LaTeX

$$Nonempty(OreSet S) ↔ ∀ r ∈ R, s ∈ S, ∃ r' ∈ R, ∃ s' ∈ S, s' r = r' s$$

Lean4

theorem nonempty_oreSet_iff_of_noZeroDivisors {R : Type*} [Ring R] [NoZeroDivisors R] {S : Submonoid R} :
    Nonempty (OreSet S) ↔ ∀ (r : R) (s : S), ∃ (r' : R) (s' : S), s' * r = r' * s :=
  by
  constructor
  · exact fun ⟨_⟩ ↦ fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩
  · intro H
    choose r' s' h using H
    exact ⟨oreSetOfNoZeroDivisors r' s' h⟩

Похожие утверждения