fixedField_antitone

Mathlib.FieldTheory.Galois.Basic

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

English

The map sending a subgroup to its fixed field is antitone with respect to inclusion.

Русский

Отображение подгруппы в фиксированное поле антимонотонно относительно включения.

LaTeX

$$$\text{Antitone}(\text{fixedField})$$$

Lean4

theorem fixedField_antitone : Antitone (@fixedField F _ E _ _) := fun _ _ ↦ fixedField_le

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

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

Разделы

Аффилиация

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