fixedField_le

Mathlib.FieldTheory.Galois.Basic

URI: https://scilib.ai/kg/mathlib#IntermediateField.fixedField_le

English

The map H ↦ fixedField H is antitone: larger H yields smaller fixed field.

Русский

Отображение H ↦ fixedField(H) антимонотонно: чем больше H, тем меньше фиксированное поле.

LaTeX

$$Antitone fixedField$$

Lean4

theorem fixedField_le {H1 H2 : Subgroup (E ≃ₐ[F] E)} (h12 : H1 ≤ H2) : fixedField H2 ≤ fixedField H1 :=
  fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h12 hx⟩

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

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

Разделы

Аффилиация

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