English
Mapping a finite-dimensional intermediate field along an algebra isomorphism preserves finite dimensionality: if E is finite-dimensional, then E.map f is finite-dimensional.
Русский
Отображение конечномерного промежуточного поля по алгебраическому эквиваленту сохраняет конечномерность: если E конечно по K, то E.map f конечно по K.
LaTeX
$$$ (f : L \to_[K] L) [FiniteDimensional K E] : FiniteDimensional K (E.map f) $$$
Lean4
/-- Mapping a finite-dimensional intermediate field along an algebra equivalence gives
a finite-dimensional intermediate field. -/
instance finiteDimensional_map (f : L →ₐ[K] L) [FiniteDimensional K E] : FiniteDimensional K (E.map f) :=
LinearEquiv.finiteDimensional (IntermediateField.equivMap E f).toLinearEquiv