adjoin_rank_eq_rank_right — Mathlib

English

If A and B are linearly disjoint with A free and B flat, then the rank of Adjoin_A(B) over A equals the rank of B over R.

Русский

Если A и B линейно диссоциированы, A свободен, а B плосок, то ранг присоединения B к A над A равен ранг B над R.

LaTeX

$$$\\operatorname{rank}_A\\big(\\operatorname{Algebra.adjoin}_A(B)\\big) = \\operatorname{rank}_R(B).$$$

Lean4

/-- If `A` and `B` are linearly disjoint, if `B` is free and `A` is flat,
then `[A[B] : A] = [B : R]`. See also `Subalgebra.adjoin_rank_le`. -/
theorem adjoin_rank_eq_rank_right [Module.Free R B] [Module.Flat R A] [Nontrivial R] [Nontrivial S] :
    Module.rank A (Algebra.adjoin A (B : Set S)) = Module.rank R B :=
  H.symm.adjoin_rank_eq_rank_left

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