ofAdjoinEqTop' — Mathlib

English

If x generates S over R and x is integral, then PowerBasis.ofAdjoinEqTop' hx hx' defines a power basis for S over R.

Русский

Если x порождает S над R и интеграл над R, то PowerBasis.ofAdjoinEqTop' hx hx' задаёт базис мощности для S над R.

LaTeX

$$$\\text{PowerBasis.ofAdjoinEqTop}'(hx, hx') : \\text{PowerBasis } R S$$$

Lean4

/-- If `x` generates `S` over `R` and is integral over `R`, then it defines a power basis.
See `PowerBasis.ofAdjoinEqTop` for a version over a field.
-/
noncomputable def _root_.PowerBasis.ofAdjoinEqTop' {x : S} (hx : IsIntegral R x) (hx' : adjoin R { x } = ⊤) :
    PowerBasis R S :=
  (adjoin.powerBasis' hx).map ((Subalgebra.equivOfEq _ _ hx').trans Subalgebra.topEquiv)

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