English
If L is a subalgebra of K over F and bL is a basis of L as an F-vector space, then the submodule generated by adjoin_E(L) equals the span over E of the range of bL.
Русский
Если L является подалгеброй K над F и bL — база L как вектора над F, то подмодуль, порождаемый adjoin_E(L), равен span_E( range bL ).
LaTeX
$$$\\operatorname{toSubmodule}(\\operatorname{adjoin}_E (L : Set K)) = \\operatorname{span}_E\\bigl(\\operatorname{range}((b_L)\\bigr)$$$
Lean4
/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F`,
then `E[L]` is generated by any basis of `L / F` as an `E`-module. -/
theorem adjoin_eq_span_basis {ι : Type*} (bL : Basis ι F L) :
toSubmodule (adjoin E (L : Set K)) = span E (Set.range fun i : ι ↦ (bL i).1) :=
L.adjoin_eq_span_of_eq_span E <| by
simpa only [← L.range_val, Submodule.map_span, Submodule.map_top, ← Set.range_comp] using
congr_arg (Submodule.map L.val) bL.span_eq.symm
