instIsMultiplicativeSchemeIsSmoothOfRelativeDimensionOfNatNat

English

The property of being smooth of relative dimension 0 is multiplicative: it is stable under identities and composition.

Русский

Свойство гладкости относительной размерности 0 сохраняется при единицах и композициях.

LaTeX

$$IsMultiplicative(IsSmoothOfRelativeDimension 0)$$

Lean4

/-- Smooth of relative dimension `0` is multiplicative. -/
instance : MorphismProperty.IsMultiplicative (@IsSmoothOfRelativeDimension 0)
    where
  id_mem _ := inferInstance
  comp_mem _ _ _ _ := inferInstance

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