ofClass

Mathlib.RingTheory.NonUnitalSubsemiring.Defs

URI: https://scilib.ai/kg/mathlib#NonUnitalSubsemiring.ofClass

Lean4

/-- The actual `NonUnitalSubsemiring` obtained from an element of a `NonUnitalSubsemiringClass`. -/
@[simps]
def ofClass {S R : Type*} [NonUnitalNonAssocSemiring R] [SetLike S R] [NonUnitalSubsemiringClass S R] (s : S) :
    NonUnitalSubsemiring R where
  carrier := s
  add_mem' := add_mem
  zero_mem' := zero_mem _
  mul_mem' := mul_mem

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

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

Разделы

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

Аффилиация

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