English
A characterization lemma for multiplication on the Ore localization, delivering Ore witnesses and conditions bundled in a sigma type: there exist r', s' with s' * r₁ = r' * s₂ and (r₁ /ₒ s₁) * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁).
Русский
Характеризационная лемма умножения в локализации Оре с существованием свидетелей в сигма-типе: существуют r', s' такие что s'·r₁ = r'·s₂ и (r₁ /ₒ s₁) * (r₂ /ₒ s₂) = r'·r₂ /ₒ (s'·s₁).
LaTeX
$$$ (r_1 /ₒ s_1) * (r_2 /ₒ s_2) = r' * r_2 /ₒ (s' * s_1) \quad \text{при } s' * r_1 = r' * s_2 $$$
Lean4
/-- A characterization lemma for the multiplication on the Ore localization, allowing for a choice
of Ore numerator and Ore denominator. -/
@[to_additive /-- A characterization lemma for the addition on the Ore localization,
allowing for a choice of Ore minuend and Ore subtrahend. -/
]
theorem oreDiv_mul_char (r₁ r₂ : R) (s₁ s₂ : S) (r' : R) (s' : S) (huv : s' * r₁ = r' * s₂) :
r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁) := by with_unfolding_all exact smul'_char r₁ r₂ s₁ s₂ s' r' huv
