isUnramified_self

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

URI: https://scilib.ai/kg/mathlib#NumberField.InfinitePlace.isUnramified_self

English

Let w be an infinite place of the field K. Then w is unramified over K (trivially, since the base is the same field).

Русский

Пусть w — бесконечное место поля K. Тогда w нерасхожено над K (это тривиально, поскольку база та же самая).

LaTeX

$$$\\operatorname{IsUnramified}(K,w)$$$

Lean4

theorem isUnramified_self : IsUnramified K w :=
  rfl

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

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

Разделы

Аффилиация

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