relfinrank_bot_left

Mathlib.FieldTheory.Relrank

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

English

The relfinrank of the bottom field over A equals the finrank of F over A.

Русский

Relfinrank нуля над A равен финитной размерности F над A.

LaTeX

$$$ \operatorname{relfinrank} \bot A = \operatorname{finrank} F A $$$

Lean4

@[simp]
theorem relfinrank_bot_left : relfinrank ⊥ A = finrank F A := by simp [relfinrank_eq_toNat_relrank, finrank]

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

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

Разделы

Аффилиация

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