instIsTotallyRealSubtypeMemSubfield

Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

URI: https://scilib.ai/kg/mathlib#NumberField.instIsTotallyRealSubtypeMemSubfield

English

IsUnramifiedIn K w is the property that every place above w is unramified over k.

Русский

IsUnramifiedIn K w — это свойство каждого места над w является безразветвлённым над k.

LaTeX

$$IsUnramifiedIn (w) := ∀ v, comap v (algebraMap k K) = w → IsUnramified k v$$

Lean4

instance [IsTotallyReal K] (F : Subfield K) : IsTotallyReal F :=
  IsTotallyReal.of_algebra F K

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

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

Разделы

Аффилиация

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