oreDiv_mul_oreDiv — Mathlib

English

The multiplication of two Ore fractions is given by the Ore product rule: (r₁ /ₒ s₁) * (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁).

Русский

Произведение двух дробей Оре задаётся правилом произведения: (r₁ /ₒ s₁) * (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁).

LaTeX

$$$ (r_1 /ₒ s_1) * (r_2 /ₒ s_2) = oreNum\,r_1\,s_2 \; \cdot \; r_2 /ₒ (oreDenom\,r_1\,s_2 \cdot s_1) $$$

Lean4

@[to_additive]
theorem oreDiv_mul_oreDiv {r₁ : R} {r₂ : R} {s₁ s₂ : S} :
    (r₁ /ₒ s₁) * (r₂ /ₒ s₂) = oreNum r₁ s₂ * r₂ /ₒ (oreDenom r₁ s₂ * s₁) := by with_unfolding_all rfl

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