rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right

English

Under suitable algebraicity, the lifted rank equalities hold on both sides when comparing L and A relative to F.

Русский

При подходящей алгебраичности выполняются тождества рангов после лифта как слева, так и справа при сопоставлении L и A относительно F.

LaTeX

$$$\operatorname{rank}_L(\text{adjoin}_L(A)) = \operatorname{rank}_F(A)$ and $\operatorname{rank}_A(\text{extendScalars}) = \operatorname{rank}_F(L)$$$

Lean4

theorem rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right (H : A.LinearDisjoint L) [Algebra.IsAlgebraic F L] :
    Module.rank F L * Module.rank (adjoin L (A : Set E)) E = Module.rank A E :=
  H.rank_right_mul_adjoin_rank_eq_of_isAlgebraic (.inr ‹_›)

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