English
If E is finite-dimensional over F and P is preserved under adjoining one element, then P holds for all intermediate fields through adjoin steps.
Русский
Если E конечномерно над F и P сохраняется при присоединении одного элемента, тогда P выполняется для всех промежуточных полей через шаги адъюнкта.
LaTeX
$$[FiniteDimensional F E] ⇒ (P bot ∧ ∀ K x, P K → P (K⟮x⟯.restrictScalars F)) → ∀ K, P K$$
Lean4
instance finiteDimensional_sup [FiniteDimensional K E1] [FiniteDimensional K E2] :
FiniteDimensional K (E1 ⊔ E2 : IntermediateField K L) :=
by
let g := Algebra.TensorProduct.productMap E1.val E2.val
suffices g.range = (E1 ⊔ E2).toSubalgebra
by
have h : FiniteDimensional K (Subalgebra.toSubmodule g.range) := g.toLinearMap.finiteDimensional_range
rwa [this] at h
rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra_of_left]
