adjoin_rank_eq_rank_right_of_isAlgebraic

English

Symmetric statement to the left version; if L is algebraic over F, rank equality holds on the right.

Русский

Симметричное утверждение по отношению к правой версии; если L алгебраично над F, равенство рангов выполняется справа.

LaTeX

$$$\operatorname{rank}_A(\operatorname{extendScalars}(\dots)) = \operatorname{rank}_F(L)$$$

Lean4

/-- The same-universe version of
`IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic`. -/
theorem adjoin_rank_eq_rank_right_of_isAlgebraic (H : A.LinearDisjoint L)
    (halg : Algebra.IsAlgebraic F A ∨ 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 :=
  by simpa only [Cardinal.lift_id] using H.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic halg

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