instIsMultiplicativeScheme

Mathlib.AlgebraicGeometry.Morphisms.Flat

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

English

Flat is a multiplicative morphism property.

Русский

Flat — это свойство морфизмов, сохраняющееся при умножении (сложении) морфизмов.

LaTeX

$$Flat is multiplicative: locus for identity, composition preserved$$

Lean4

instance : MorphismProperty.IsMultiplicative @Flat where id_mem _ := inferInstance

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

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

Разделы

Аффилиация

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