instSubringClass

Mathlib.Algebra.Ring.Subring.Defs

URI: https://scilib.ai/kg/mathlib#Subring.instSubringClass

← MathLib Explorer

English

Subring R forms a SubringClass with respect to R.

Русский

Подкольцо R образует класс подкольца по отношению к R.

LaTeX

$$$ \\operatorname{SubringClass}(\\mathrm{Subring}(R), R) $$$

Lean4

instance : SubringClass (Subring R) R where
  zero_mem s := s.zero_mem'
  add_mem {s} := s.add_mem'
  one_mem s := s.one_mem'
  mul_mem {s} := s.mul_mem'
  neg_mem {s} := s.neg_mem'

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

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

Разделы

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

Аффилиация

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