smooth_def — Mathlib

English

A ring homomorphism f is Smooth if and only if it is formally smooth and of finite presentation.

Русский

Гомоморфизм гладок тогда и только тогда, когда он формально гладок и имеет конечную презентацию.

LaTeX

$$$f\text{.Smooth} \iff f\text{.FormallySmooth} \land f\text{.FinitePresentation}$$$

Lean4

theorem smooth_def {f : R →+* S} : f.Smooth ↔ f.FormallySmooth ∧ f.FinitePresentation :=
  letI := f.toAlgebra
  Algebra.smooth_iff _ _

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