instIsMultiplicativeScheme

Mathlib.AlgebraicGeometry.Morphisms.Integral

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme

English

IsIntegralHom is a multiplicative morphism property; it is stable under composition and identities respect it.

Русский

IsIntegralHom является свойством морфизмов, сохраняющимся под композицией и идентичности сохраняют это свойство.

LaTeX

$$IsMultiplicative IsIntegralHom$$

Lean4

instance : IsMultiplicative @IsIntegralHom where

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

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

Разделы

Аффилиация

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