relfinrank_mul_finrank_top

Mathlib.FieldTheory.Relrank

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

← MathLib Explorer

English

If A ≤ B, then relfinrank(A,B) · finrank(B,E) = finrank(A,E).

Русский

Если A ⊆ B, тогда relfinrank(A,B) · finrank(B,E) = finrank(A,E).

LaTeX

$$$A \le B \Rightarrow \operatorname{relfinrank} A B \cdot \operatorname{finrank} B E = \operatorname{finrank} A E$$$

Lean4

theorem relfinrank_mul_finrank_top (h : A ≤ B) : relfinrank A B * finrank B E = finrank A E := by
  simpa using congr(toNat $(relrank_mul_rank_top h))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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