rank_bot_mul_relrank — Mathlib

English

Let A and B be intermediate subfields of E over F with A ⊆ B. Then the dimension of B over F equals the dimension of A over F times the dimension of B over A.

Русский

Пусть A и B — промежуточные поля над F в E и A ⊆ B. Тогда размерность B над F равна произведению размерности A над F и размерности B над A.

LaTeX

$$$ (A \le B) \Rightarrow \operatorname{rank}_F A \cdot \operatorname{relrank} A B = \operatorname{rank}_F B $$$

Lean4

theorem rank_bot_mul_relrank (h : A ≤ B) : Module.rank F A * relrank A B = Module.rank F B :=
  by
  rw [relrank_eq_rank_of_le h]
  letI : Algebra A B := (inclusion h).toAlgebra
  haveI : IsScalarTower F A B := IsScalarTower.of_algebraMap_eq' rfl
  exact rank_mul_rank F A B

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