ofAdjoinEqTop_gen — Mathlib

English

Let x be integral over K and adjoin_K({x}) = S. Then the generator of the power basis of S over K is x.

Русский

Пусть x интеграл над K и adjoin_K({x}) = S. Тогда генератор базиса мощности S над K есть x.

LaTeX

$$$\text{PowerBasis.ofAdjoinEqTop hx hx'}.gen = x$$$

Lean4

@[simp]
theorem _root_.PowerBasis.ofAdjoinEqTop_gen {x : S} (hx : IsIntegral K x) (hx' : adjoin K { x } = ⊤) :
    (PowerBasis.ofAdjoinEqTop hx hx').gen = x :=
  rfl

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