lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right

English

If A and L are linearly disjoint over F and one of them is algebraic, then the lifted rank of the adjoin construction equals the rank of the other side over F.

Русский

Если A и L линейно независимы над F и одно из них алгебраично, то тильд-ранг адъюнкта равен рангу другой стороны над F.

LaTeX

$$$\operatorname{lift}\left(\operatorname{rank}\right) = \operatorname{lift}\left(\operatorname{rank}\right)$$

Lean4

theorem lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right (H : A.LinearDisjoint L) [Algebra.IsAlgebraic F L] :
    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 (.inr ‹_›)

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