homogeneousLocalizationCommRing — Mathlib

English

The homogeneous localization carries a commutative ring structure.

Русский

Однородная локализация обладает структурой коммутативного кольца.

LaTeX

$$$\\mathrm{HomogeneousLocalization}(\\mathcal{A},x) \\text{ is a commutative ring.}$$$

Lean4

instance homogeneousLocalizationCommRing : CommRing (HomogeneousLocalization 𝒜 x) :=
  (HomogeneousLocalization.val_injective x).commRing _ val_zero val_one val_add val_mul val_neg val_sub
    (val_nsmul x · ·) (val_zsmul x · ·) val_pow val_natCast val_intCast

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