algHomAdjoinIntegralEquiv_symm_apply_gen

English

If h is IsIntegral F α, then the symmetry of the equivalence preserves the generator: the symm image of a root generator maps back to α.

Русский

Если h — IsIntegral F α, то симметрия эквивалента сохраняет индукцию: образ симметричного отображения корня возвращает α.

LaTeX

$$For h : IsIntegral F α and x in (minpoly F α).aroots K, (algHomAdjoinIntegralEquiv F h).symm x (AdjoinSimple.gen F α) = x$$

Lean4

theorem algHomAdjoinIntegralEquiv_symm_apply_gen (h : IsIntegral F α) (x : { x // x ∈ (minpoly F α).aroots K }) :
    (algHomAdjoinIntegralEquiv F h).symm x (AdjoinSimple.gen F α) = x :=
  (adjoin.powerBasis h).lift_gen x.val <| by rw [adjoin.powerBasis_gen, minpoly_gen]; exact (mem_aroots.mp x.2).2

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