oreDiv_smul_oreDiv — Mathlib

English

The action of an Ore fraction (r₁ /ₒ s₁) on another fraction (r₂ /ₒ s₂) is given by the Ore numerator/denominator data: (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁).

Русский

Действие дроби Ore (r₁ /ₒ s₁) на другую дробь (r₂ /ₒ s₂) задаётся данными числителя/знаменателя Ore: (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁).

LaTeX

$$$ (r_1 /ₒ s_1) \; \bullet \; (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_smul_oreDiv {r₁ : R} {r₂ : X} {s₁ s₂ : S} :
    (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) := by with_unfolding_all rfl

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