English
If r ∈ K and g: (minpoly K x).Splits (algebraMap K L), then (minpoly K (x + algebraMap K L r)).Splits (algebraMap K L).
Русский
Если r ∈ K и minpoly K x распадается в L, то minpoly K (x + algebraMap K L r) распадается в L.
LaTeX
$$$\\text{Splits}(\\operatorname{algebraMap} K L, \\minpoly K(x + \\operatorname{algebraMap} K L r))$$$
Lean4
/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F`,
then `[E[L] : E] ≤ [L : F]`. -/
theorem adjoin_rank_le {F : Type*} (E : Type*) {K : Type*} [CommSemiring F] [StrongRankCondition F] [CommSemiring E]
[StrongRankCondition E] [Semiring K] [SMul F E] [Algebra E K] [Algebra F K] [IsScalarTower F E K]
(L : Subalgebra F K) [Module.Free F L] : Module.rank E (Algebra.adjoin E (L : Set K)) ≤ Module.rank F L :=
by
rw [← rank_toSubmodule, Module.Free.rank_eq_card_chooseBasisIndex F L,
L.adjoin_eq_span_basis E (Module.Free.chooseBasis F L)]
exact rank_span_le _ |>.trans Cardinal.mk_range_le
