finrank_right_eq_finrank — Mathlib

English

If A and B are linearly disjoint over F and A ⊔ B = E, then the dimension of E over B equals the dimension of A over F: [E : B] = [A : F].

Русский

Если A и B линейно независимы над F и A ⊔ B = E, то [E : B] = [A : F].

LaTeX

$$$\operatorname{finrank}_B(E) = \operatorname{finrank}_F(A)$$$

Lean4

/-- If `A` and `B` are linearly disjoint over `F` and `A ⊔ B = E`, then the `Module.finrank` of
`E` over `B` is equal to the `Module.finrank` of `A` over `F`.
-/
theorem finrank_right_eq_finrank [Module.Finite F B] (h₁ : A.LinearDisjoint B) (h₂ : A ⊔ B = ⊤) :
    finrank B E = finrank F A :=
  h₁.symm.finrank_left_eq_finrank (by rwa [sup_comm])

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