oreDiv_mul_oreDiv_comm — Mathlib

English

Let R be a commutative monoid and S a submonoid satisfying the Ore condition. Then in the Ore localization R[S⁻¹], the product of two fractions r1/s1 and r2/s2 is given by (r1 r2)/(s1 s2).

Русский

Пусть R — коммутативный моноид и S — подмоноид, удовлетворяющий условию Оре. Тогда в локализации Оре R[S⁻¹] произведение двух дробей r1/s1 и r2/s2 равно (r1 r2)/(s1 s2).

LaTeX

$$$ (r_1 /_\\o s_1) \\cdot (r_2 /_\\o s_2) = (r_1 r_2) /_\\o (s_1 s_2) $$$

Lean4

@[to_additive]
theorem oreDiv_mul_oreDiv_comm {r₁ r₂ : R} {s₁ s₂ : S} : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂) := by
  rw [oreDiv_mul_char r₁ r₂ s₁ s₂ r₁ s₂ (by simp [mul_comm]), mul_comm s₂]

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