English
If x is integral over K and adjoin_K({x}) equals the whole S, then transporting the power basis of adjoin_K({x}) along the natural equivalence with S yields a power basis of S over K.
Русский
Если x интеграл над K и adjoin_K({x}) = S, то базис мощности adjoin_K({x}) передается через естественное эквивилирование на S, образуя базис S над K.
LaTeX
$$$\\text{PowerBasis.ofAdjoinEqTop}(hx,hx') = (\\mathrm{adjoin}_K(\\{x\\})).powerBasis \\text{ перенесённый по}\; (\\mathrm{Subalgebra.equivOfEq}\\ to \\text{topEquiv})$$$
Lean4
/-- If `x` generates `S` over `K` and is integral over `K`, then it defines a power basis.
See `PowerBasis.ofAdjoinEqTop'` for a version over a more general base ring.
-/
noncomputable def _root_.PowerBasis.ofAdjoinEqTop {x : S} (hx : IsIntegral K x) (hx' : adjoin K { x } = ⊤) :
PowerBasis K S :=
(adjoin.powerBasis hx).map ((Subalgebra.equivOfEq _ _ hx').trans Subalgebra.topEquiv)
