of_id

Mathlib.RingTheory.EssentialFiniteness

URI: https://scilib.ai/kg/mathlib#Algebra.EssFiniteType.of_id

English

Every ring is essentially of finite type over itself.

Русский

Каждое кольцо по сути является кольцом конечного типа над самим собой.

LaTeX

$$$EssFiniteType\, R\, R$$$

Lean4

theorem of_id : EssFiniteType R R :=
  inferInstance

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

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

Разделы

Аффилиация

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