English
A sigma-form characterization of multiplication: there exist r' and s' such that 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
$$$ \exists r', s' : R, S, s' * r_1 = r' * s_2 \wedge r_1 /ₒ s_1 * (r_2 /ₒ s_2) = r' * r_2 /ₒ (s' * s_1) $$$
Lean4
/-- Another characterization lemma for the multiplication on the Ore localization delivering
Ore witnesses and conditions bundled in a sigma type. -/
@[to_additive /-- Another characterization lemma for the addition on the Ore localization delivering
Ore witnesses and conditions bundled in a sigma type. -/
]
def oreDivMulChar' (r₁ r₂ : R) (s₁ s₂ : S) :
Σ' r' : R, Σ' s' : S, s' * r₁ = r' * s₂ ∧ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁) :=
⟨oreNum r₁ s₂, oreDenom r₁ s₂, ore_eq r₁ s₂, oreDiv_mul_oreDiv⟩
