English
A characterization lemma for scalar multiplication on the Ore localization: if there exist r' and s' with s' * r₁ = r' * s₂, then (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) \; \ast \; (r_2 /ₒ s_2) = r' \; \cdot \; r_2 /ₒ (s' \cdot s_1) \quad \text{при } s' \cdot r_1 = r' \cdot s_2 $$$
Lean4
/-- A characterization lemma for the scalar multiplication on the Ore localization,
allowing for a choice of Ore numerator and Ore denominator. -/
@[to_additive /-- A characterization lemma for the vector addition on the Ore localization,
allowing for a choice of Ore minuend and Ore subtrahend. -/
]
theorem oreDiv_smul_char (r₁ : R) (r₂ : X) (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
