relfinrank_top_right

Mathlib.FieldTheory.Relrank

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

English

The relfinrank of A over the top field equals the finrank of A over E.

Русский

Relfinrank поля A над верхним полем равен финитной размерности A над E.

LaTeX

$$$ \operatorname{relfinrank} A \top = \operatorname{finrank} A E $$$

Lean4

@[simp]
theorem relfinrank_top_right : relfinrank A ⊤ = finrank A E := by simp [relfinrank_eq_toNat_relrank, finrank]

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

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

Разделы

Аффилиация

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