instRing — Mathlib

English

If A is a Ring and S a submonoid, LocalizedModule S A inherits a ring structure (in particular, the additive and multiplicative structures are compatible).

Русский

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

LaTeX

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

Lean4

instance {A : Type*} [Ring A] [Algebra R A] {S : Submonoid R} : Ring (LocalizedModule S A) :=
  { inferInstanceAs (AddCommGroup (LocalizedModule S A)), inferInstanceAs (Semiring (LocalizedModule S A)) with }

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