English
If L is a subalgebra of K over F and h says toSubmodule L = span_F S, then toSubmodule (adjoin E (L : Set K)) = span_E S. In words: if the subalgebra L is generated by S as an F-module, then the E-submodule generated by L is generated by S over E.
Русский
Если L — подалгебра K над F и выполняется toSubmodule L = span_F S, то toSubmodule (adjoin E (L : Set K)) = span_E S. Другими словами: если L порождается S как F-модуль, то E-подмодуль, порожденный L, порождается S над E.
LaTeX
$$$ \operatorname{toSubmodule}(\operatorname{adjoin}_{E} (L : Set K)) = \operatorname{span}_{E} S $$$
Lean4
/-- If `K / E / F` is a ring extension tower, `L` is a subalgebra of `K / F` which is generated by
`S` as an `F`-module, then `E[L]` is generated by `S` as an `E`-module. -/
theorem adjoin_eq_span_of_eq_span {S : Set K} (h : toSubmodule L = span F S) :
toSubmodule (adjoin E (L : Set K)) = span E S :=
L.toSubmonoid.adjoin_eq_span_of_eq_span F E (congr_arg ((↑) : _ → Set K) h)
