of_isScalarTower — Mathlib

English

Equivalence of ConjRoot and orbitRel relation under normal extension.

Русский

Эквивалентность между сопряжённостью и отношением орбиты при нормальном расширении.

LaTeX

$$$IsConjRoot(K, x, y) \iff MulAction.orbitRel (AlgEquiv(K, L, L)) L x y$$$

Lean4

/-- Let `S / L / K` be a tower of extensions. For any two elements `y` and `x` in `S`, if `y` is a
conjugate root of `x` over `L`, then `y` is also a conjugate root of `x` over
`K`.
-/
theorem of_isScalarTower [IsScalarTower K L S] {x y : S} (hx : IsIntegral K x) (h : IsConjRoot L x y) :
    IsConjRoot K x y :=
  isConjRoot_of_aeval_eq_zero hx <| minpoly.aeval_of_isScalarTower K x y (aeval_eq_zero h)

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