instCommMonoid — Mathlib

English

If R is a commutative monoid and S is an Ore set, then the Ore localization R[S⁻¹] is a commutative monoid.

Русский

Если R — коммутативный моноид, а S — множество Оре, то локализация Оре R[S⁻¹] является коммутативным моноидом.

LaTeX

$$$R[S^{-1}] \text{ is a commutative monoid}$$$

Lean4

@[to_additive]
instance : CommMonoid R[S⁻¹] where
  mul_comm := fun x y =>
    by
    cases x with
    | _ r₁ s₁
    cases y with
    | _ r₂ s₂
    rw [oreDiv_mul_oreDiv_comm, oreDiv_mul_oreDiv_comm, mul_comm r₁, mul_comm s₁]

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