nonempty_oreSet_iff — Mathlib

English

A nonempty OreSet exists iff two conditions of Ore-cancellation and division rules hold.

Русский

Существование непустого OreSet эквивалентно двум условиям: отмена в Ore и существование коэффициентов, удовлетворяющих соотношению.

LaTeX

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

Lean4

theorem nonempty_oreSet_iff {R : Type*} [Monoid R] {S : Submonoid R} :
    Nonempty (OreSet S) ↔
      (∀ (r₁ r₂ : R) (s : S), r₁ * s = r₂ * s → ∃ s' : S, s' * r₁ = s' * r₂) ∧
        (∀ (r : R) (s : S), ∃ (r' : R) (s' : S), s' * r = r' * s) :=
  by
  constructor
  · exact fun ⟨_⟩ ↦ ⟨ore_right_cancel, fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩⟩
  · intro ⟨H, H'⟩
    choose r' s' h using H'
    exact ⟨H, r', s', h⟩

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