self

Mathlib.RingTheory.FinitePresentation

URI: https://scilib.ai/kg/mathlib#Algebra.FinitePresentation.self

← MathLib Explorer

English

R is finitely presented as a ring over itself.

Русский

R как кольцо над R имеет конечную презентацию.

LaTeX

$$$\\text{FinitePresentation } R R$$$

Lean4

/-- `R` is finitely presented as `R`-algebra. -/
instance self : FinitePresentation R R :=
  have := FinitePresentation.mvPolynomial_aux R Empty
  equiv (MvPolynomial.isEmptyAlgEquiv R Empty)

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

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

Разделы

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

Аффилиация

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