unop

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

URI: https://scilib.ai/kg/mathlib#Subsemiring.unop

Lean4

/-- Pull an opposite subsemiring back to a subsemiring along `MulOpposite.op` -/
@[simps! coe toSubmonoid]
protected def unop (S : Subsemiring Rᵐᵒᵖ) : Subsemiring R
    where
  toSubmonoid := S.toSubmonoid.unop
  add_mem' {x} {y} hx hy := add_mem (show MulOpposite.op x ∈ S from hx) (show MulOpposite.op y ∈ S from hy)
  zero_mem' := zero_mem S

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

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

Разделы

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

Аффилиация

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