equivAdjoinSimple_symm_gen — Mathlib

English

If minpoly K x equals minpoly K y, then the corresponding algEquiv on the two adjoined fields matches the symmetry.

Русский

Если minpoly K x совпадает с minpoly K y, тогда соответствующее эквив между адъюнктами совпадает с симметрией.

LaTeX

$$minpoly.algEquiv (hx) (h_mp) and its symmetry$$

Lean4

@[simp]
theorem equivAdjoinSimple_symm_gen (pb : PowerBasis K L) :
    pb.equivAdjoinSimple.symm pb.gen = AdjoinSimple.gen K pb.gen := by
  rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_gen, adjoin.powerBasis_gen]

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