finrank_left_eq_finrank — Mathlib

English

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

Русский

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

LaTeX

$$$\operatorname{finrank}_A(E) = \operatorname{finrank}_F(B)$$$

Lean4

/-- If `A` and `B` are linearly disjoint over `F` and `A ⊔ B = E`, then the `Module.finrank` of
`E` over `A` is equal to the `Module.finrank` of `B` over `F`.
-/
theorem finrank_left_eq_finrank [Module.Finite F A] (h₁ : A.LinearDisjoint B) (h₂ : A ⊔ B = ⊤) :
    finrank A E = finrank F B := by
  have := h₁.finrank_sup
  rwa [h₂, finrank_top', ← finrank_mul_finrank F A E, mul_right_inj' finrank_pos.ne'] at this

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