adjoin_rank_eq_rank_right_of_isAlgebraic_left

English

If the finite ranks [F: A] and [F: L] are coprime, then A and L are linearly disjoint over F.

Русский

Если степени A и L над F являются взаимно простыми, то A и L линейно независимы над F.

LaTeX

$$$\operatorname{coprime}(\operatorname{finrank}_F A, \operatorname{finrank}_F L) \Rightarrow A \perp L$$

Lean4

theorem adjoin_rank_eq_rank_right_of_isAlgebraic_left (H : A.LinearDisjoint L) [Algebra.IsAlgebraic F A] :
    Module.rank A (extendScalars (show A ≤ (adjoin L (A : Set E)).restrictScalars F from subset_adjoin L (A : Set E))) =
      Module.rank F L :=
  H.adjoin_rank_eq_rank_right_of_isAlgebraic (.inl ‹_›)

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