instRingRestrictScalars

Mathlib.Algebra.Algebra.RestrictScalars

URI: https://scilib.ai/kg/mathlib#instRingRestrictScalars

English

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

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru