finite

Mathlib.RingTheory.Localization.Basic

URI: https://scilib.ai/kg/mathlib#IsLocalization.finite

← MathLib Explorer

English

If R is finite and S is a localization of R, then S is finite as well.

Русский

Если кольцо R конечно, то и локализация S является конечной.

LaTeX

$$$[\\Finite(R)] \\Rightarrow [\\Finite(S)]$$$

Lean4

protected theorem finite [Finite R] : Finite S :=
  by
  have : Function.Surjective (Function.uncurry (mk' (M := M) S)) := fun x ↦ by
    simpa using IsLocalization.mk'_surjective M x
  exact .of_surjective _ this

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

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

Разделы

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

Аффилиация

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