adjoin_rank_eq_rank_left_of_isAlgebraic_left

English

If H: A is linearly disjoint with L and A is algebraic over F, then [L(A) : L] = [A : F].

Русский

Если A линейно совместим с L и A алгебраично над F, тогда [L(A) : L] = [A : F].

LaTeX

$$$[L(A) : L] = [A : F]$$$

Lean4

theorem adjoin_rank_eq_rank_left_of_isAlgebraic_left (H : A.LinearDisjoint L) [Algebra.IsAlgebraic F A] :
    Module.rank L (adjoin L (A : Set E)) = Module.rank F A :=
  H.adjoin_rank_eq_rank_left_of_isAlgebraic (.inl ‹_›)

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