instSemiringRestrictScalars — Mathlib

English

The restricted scalar construction inherits a semiring structure from A: RestrictScalars R S A is a semiring when A is a semiring.

Русский

У конструкции ограничения скаляров наследуется структура полупрямого кольца от A: RestrictScalars R S A является полукольцом, если A — полукольцо.

LaTeX

$$$\text{Semiring}(\mathrm{RestrictScalars}(R,S,A))$$$

Lean4

instance [I : Semiring A] : Semiring (RestrictScalars R S A) :=
  I

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