oreDiv_eq_iff — Mathlib

English

Two fractions r1/s1 and r2/s2 are equal in the Ore localization iff there exist u ∈ S and v ∈ R with ur2 = vr1 and us2 = vs1.

Русский

Две дроби r1/s1 и r2/s2 равны в Ore локализации тогда и только тогда, когда существуют u ∈ S и v ∈ R такие, что u r2 = v r1 и u s2 = v s1.

LaTeX

$$r1 / s1 = r2 / s2 ⇔ ∃u ∈ S ∃v ∈ R, u·r2 = v·r1 ∧ u·s2 = v·s1$$

Lean4

@[to_additive]
theorem oreDiv_eq_iff {r₁ r₂ : X} {s₁ s₂ : S} :
    r₁ /ₒ s₁ = r₂ /ₒ s₂ ↔ ∃ (u : S) (v : R), u • r₂ = v • r₁ ∧ u * s₂ = v * s₁ :=
  Quotient.eq''

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