lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left

English

If A and L are linearly disjoint over F and L is algebraic over F, then a symmetric lifted rank equality holds as in the left variant.

Русский

Если A и L линейно независимы над F и L алгебраично над F, тогда существует симметричное тождество рангов после лифта.

LaTeX

$$$\text{lifted rank equality (right variant)}$$$

Lean4

theorem lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left (H : A.LinearDisjoint L) [Algebra.IsAlgebraic F A] :
    Cardinal.lift.{w}
        (Module.rank A
          (extendScalars (show A ≤ (adjoin L (A : Set E)).restrictScalars F from subset_adjoin L (A : Set E)))) =
      Cardinal.lift.{v} (Module.rank F L) :=
  H.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic (.inl ‹_›)

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