adjoin_rank_eq_rank_right_of_isAlgebraic_right

English

The same-universe version of lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic; equality holds without lifting across universes when the algebraic condition is met.

Русский

Аналогичная вселенская версия для lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic; равенство сохраняется без переносов между вселенными при условии алгебраичности.

LaTeX

$$$\operatorname{lift}([\cdot]) = \operatorname{lift}([\cdot])$$$

Lean4

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

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