instIsSmooth

Mathlib.AlgebraicGeometry.Morphisms.Etale

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsEtale.instIsSmooth

English

If f: X → Y is étale, then f is smooth.

Русский

Если отображение f: X → Y является étale, тогда оно гладкое (smooth).

LaTeX

$$$\\text{IsEtale}(f)\\implies \\text{IsSmooth}(f)$$$

Lean4

instance [IsEtale f] : IsSmooth f :=
  IsSmoothOfRelativeDimension.isSmooth 0 f

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

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

Разделы

Аффилиация

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