essFiniteType

Mathlib.RingTheory.EssentialFiniteness

URI: https://scilib.ai/kg/mathlib#RingHom.FiniteType.essFiniteType

English

If a ring hom is of finite type, then it is essentially of finite type.

Русский

Если гомоморфизм кольца конечного типа, то он является существенно конечного типа.

LaTeX

$$$f:\,R\to S\text{ finite type} \Rightarrow f:\,R\to S\text{ EssFiniteType}$$$

Lean4

theorem essFiniteType (hf : f.FiniteType) : f.EssFiniteType :=
  by
  algebraize [f]
  change Algebra.EssFiniteType R S
  infer_instance

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

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

Разделы

Аффилиация

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