rank_bot

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

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

English

The bottom intermediate field has rank 1 over F.

Русский

Нижнее промежуточное поле имеет ранг 1 над F.

LaTeX

$$Module.rank F ⊥ = 1$$

Lean4

@[simp]
protected theorem rank_bot : Module.rank F (⊥ : IntermediateField F E) = 1 := by rw [rank_eq_one_iff]

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

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

Разделы

Аффилиация

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