isStandardSmooth — Mathlib

English

For every n, if f has IsStandardSmoothOfRelativeDimension n f, then f is IsStandardSmooth.

Русский

Для каждого n, если f имеет IsStandardSmoothOfRelativeDimension n f, тогда f является IsStandardSmooth.

LaTeX

$$$\forall n, \; f: R \to S, \; \mathrm{IsStandardSmoothOfRelativeDimension}(n)(f) \Rightarrow \mathrm{IsStandardSmooth}(f)$$$

Lean4

theorem isStandardSmooth (f : R →+* S) (hf : IsStandardSmoothOfRelativeDimension n f) : IsStandardSmooth f :=
  by
  algebraize [f]
  exact Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth n

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