English
A sigma-valued characterization: there exists a pair of Ore witnesses (r', s') such that s' * r₁ = r' * s₂ and the equality (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁) holds, packaged in a sigma type.
Русский
Сигма-характеризация: существует пара свидетелей Оре (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) \; \cdot \; (r_2 /ₒ s_2) = r' \cdot r_2 /ₒ (s' \cdot s_1) $$$
Lean4
/-- Another characterization lemma for the scalar multiplication on the Ore localization delivering
Ore witnesses and conditions bundled in a sigma type. -/
@[to_additive /-- Another characterization lemma for the vector addition on the
Ore localization delivering Ore witnesses and conditions bundled in a sigma type. -/
]
def oreDivSMulChar' (r₁ : R) (r₂ : X) (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_smul_oreDiv⟩
