finrank_bot_mul_relfinrank — Mathlib

English

If A ⊆ B are intermediate F-subfields of E, then finrank F B = finrank F A × relfinrank A B (finite dimensions assumed).

Русский

Если A ⊆ B — промежуточные поля над F в E, то finrank F B = finrank F A × relfinrank A B (при конечных размерностях).

LaTeX

$$$ (A \le B) \Rightarrow \operatorname{finrank} F B = \operatorname{finrank} F A \cdot \operatorname{relfinrank} A B $$$

Lean4

theorem finrank_bot_mul_relfinrank (h : A ≤ B) : finrank F A * relfinrank A B = finrank F B := by
  simpa using congr(toNat $(rank_bot_mul_relrank h))

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