toNonUnitalRing

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalSubalgebra.toNonUnitalRing

English

An instance provides that a NonUnitalSubalgebra S inherits a NonUnitalSemiring structure.

Русский

Экземпляр обеспечивает, что подпалгебра S наследует структуру NonUnitalSemiring.

LaTeX

$$[NonUnitalSubsemiring] (S) := \text{instance}$$

Lean4

instance toNonUnitalRing [CommRing R] [NonUnitalRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalRing S :=
  inferInstance

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

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

Разделы

Аффилиация

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