smooth_algebraMap

Mathlib.RingTheory.RingHom.Smooth

URI: https://scilib.ai/kg/mathlib#RingHom.smooth_algebraMap

English

For an algebra map, smoothness of the map is equivalent to smoothness of the algebra.

Русский

Для алгебраMap гладкость отображения эквивалентна гладкости алгебры.

LaTeX

$$$(\text{algebraMap } R S).\text{Smooth} \iff \mathrm{Algebra.Smooth}(R,S)$$$

Lean4

theorem smooth_algebraMap [Algebra R S] : (algebraMap R S).Smooth ↔ Algebra.Smooth R S := by
  rw [RingHom.Smooth, toAlgebra_algebraMap]

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

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

Разделы

Аффилиация

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