finiteDimensional_map — Mathlib

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

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