rootOfSplitsXPowSubC_pow — Mathlib

English

In the splitting field L of X^n − C a, the nth power of the chosen rootOfSplitsXPowSubC equals algebraMap a in L, i.e., α^n = a under the canonical map.

Русский

В разворачивающем поле L для X^n − C a соответствие α^n = a выполняется по отношению к каноническому отображению.

LaTeX

$$$\left(\text{rootOfSplitsXPowSubC}(\mathrm{pos}\, n, a, L)\right)^n = \mathrm{algebraMap}_{K,L}(a).$$$

Lean4

theorem rootOfSplitsXPowSubC_pow [NeZero n] : (rootOfSplitsXPowSubC (NeZero.pos n) a L) ^ n = algebraMap K L a :=
  by
  have := map_rootOfSplits _ (IsSplittingField.splits L (X ^ n - C a))
  simp only [eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero] at this
  exact this _

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