toAlgebra — Mathlib

English

If IsStandardSmooth n f holds, then f.toAlgebra is IsStandardSmoothOfRelativeDimension n.

Русский

Если f является стандартно гладким относительного размерности n, то f.toAlgebra имеет соответствующую гладкость по размерности.

LaTeX

$$$\mathrm{IsStandardSmooth(n)}(f) \Rightarrow \mathrm{IsStandardSmoothOfRelativeDimension}(n)(f^{\text{algebra}})$$$

Lean4

/-- Helper lemma for the `algebraize` tactic -/
theorem toAlgebra {f : R →+* S} (hf : IsStandardSmooth f) : @Algebra.IsStandardSmooth R S _ _ f.toAlgebra :=
  hf

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