instCommRing — Mathlib

English

If A is a commutative ring and S is a submonoid, the localized module LocalizedModule S A becomes a commutative ring, i.e., the multiplication is commutative.

Русский

Если A — коммутативное кольцо и S — подмоноид, то локализованный модуль LocalizedModule S A становится коммутативным кольцом, то есть умножение коммутативно.

LaTeX

$$$\\mathrm{LocalizedModule}(S,A)$ is a CommRing$$

Lean4

instance {A : Type*} [CommRing A] [Algebra R A] {S : Submonoid R} : CommRing (LocalizedModule S A) :=
  { show (Ring (LocalizedModule S A)) by infer_instance with
    mul_comm := by
      rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩
      exact mk_eq.mpr ⟨1, by simp only [one_smul, mul_comm]⟩ }

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