instIsIntegralHom

Mathlib.AlgebraicGeometry.Morphisms.Finite

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsFinite.instIsIntegralHom

English

If a morphism f is finite, then it is integral.

Русский

Если морфизм f конечен, то он интегральный.

LaTeX

$$$\mathrm{IsFinite}(f) \implies \mathrm{IsIntegralHom}(f).$$$

Lean4

instance (priority := 900) [IsFinite f] : IsIntegralHom f :=
  ((IsFinite.iff_isIntegralHom_and_locallyOfFiniteType f).mp ‹_›).1

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

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

Разделы

Аффилиация

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