of_restrictScalars

Mathlib.RingTheory.Unramified.Locus

URI: https://scilib.ai/kg/mathlib#Algebra.IsUnramifiedAt.of_restrictScalars

English

If P is unramified over R, then P is unramified over A when restricted scalars from A to R are considered.

Русский

Если P неразветвлен над R, то P неразветвлен над A при ограничении скаляров с A на R.

LaTeX

$$IsUnramifiedAt.of_restrictScalars P$$

Lean4

theorem of_restrictScalars (P : Ideal B) [P.IsPrime] [IsUnramifiedAt R P] : IsUnramifiedAt A P :=
  FormallyUnramified.of_comp R _ _

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

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

Разделы

Аффилиация

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