instMul — Mathlib

English

The Ore localization R[S⁻¹] inherits a multiplication, making it a monoid under the operations defined by the Ore localization construction.

Русский

Локализация Оре R[S⁻¹] наследует умножение, образуя моноид по операциям локализации Оре.

LaTeX

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

Lean4

@[to_additive]
instance : Mul R[S⁻¹] :=
  ⟨OreLocalization.smul⟩

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