toNonUnitalSemiring

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

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

← MathLib Explorer

English

The underlying set of the copied subalgebra equals the original carrier.

Русский

Основное множество копированной подпалгебры совпадает с исходным карриером.

LaTeX

$$$(S.copy\ s\ hs) = s$$$

Lean4

instance toNonUnitalSemiring [CommSemiring R] [NonUnitalSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) :
    NonUnitalSemiring S :=
  inferInstance

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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