English
If for all x ∈ E we have finrank F F⟮x⟯ = 1, then Subsingleton (IntermediateField F E).
Русский
Если для каждого x ∈ E finrank F F⟮x⟯ = 1, тогда Subsingleton (IntermediateField F E).
LaTeX
$$(∀ x : E, \operatorname{finrank} F F⟮x⟯ = 1) → Subsingleton (IntermediateField F E)$$
Lean4
/-- The power basis `1, x, ..., x ^ (d - 1)` for `K⟮x⟯`,
where `d` is the degree of the minimal polynomial of `x`. -/
@[simps]
noncomputable def powerBasis {x : L} (hx : IsIntegral K x) : PowerBasis K K⟮x⟯
where
gen := AdjoinSimple.gen K x
dim := (minpoly K x).natDegree
basis := powerBasisAux hx
basis_eq_pow
i := by
rw [powerBasisAux, Basis.reindex_apply, Basis.map_apply, PowerBasis.basis_eq_pow, finCongr_symm, finCongr_apply,
Fin.cast_eq_self, AlgEquiv.toLinearEquiv_apply, map_pow, AdjoinRoot.powerBasis_gen,
adjoinRootEquivAdjoin_apply_root]
