Corner

Mathlib.RingTheory.Idempotents

URI: https://scilib.ai/kg/mathlib#IsIdempotentElem.Corner

Lean4

/-- The corner associated to an idempotent `e` in a semiring without 1
is the semiring with `e` as 1 consisting of all element of the form `e * r * e`. -/
@[nolint unusedArguments]
def _root_.IsIdempotentElem.Corner (_ : IsIdempotentElem e) : Type _ :=
  Subsemigroup.corner e

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

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

Разделы

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

Аффилиация

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