ofClass

Mathlib.RingTheory.NonUnitalSubring.Defs

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

Lean4

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

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

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

Разделы

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

Аффилиация

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