lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right

English

If H: A ⊥ L and halg holds, then the left-universe version of adjoin rank equality holds.

Русский

Если H: A ⊥ L и выполняется условие алгебраичности, тогда выполняется равенство рангов слева для адъюнкта.

LaTeX

$$$\operatorname{rank}_L(\operatorname{adjoin}_L(A)) = \operatorname{rank}_F(A)$$$

Lean4

theorem lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right (H : A.LinearDisjoint L)
    [Algebra.IsAlgebraic F L] :
    Cardinal.lift.{v} (Module.rank F L) * Cardinal.lift.{w} (Module.rank (adjoin L (A : Set E)) E) =
      Cardinal.lift.{w} (Module.rank A E) :=
  H.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic (.inr ‹_›)

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