rootsEquivRoots — Mathlib

English

There is a canonical equivalence between the root set of p in p.SplittingField and the root set of p in E when p splits over E.

Русский

Существует каноническое эквивалентное отображение между множеством корней p в p.SplittingField и множеством корней p в E, если p распадается над E.

LaTeX

$$$p.rootSet\\,p.SplittingField \\cong p.rootSet\\,E$$$

Lean4

/-- The bijection between `rootSet p p.SplittingField` and `rootSet p E`. -/
def rootsEquivRoots [Fact (p.Splits (algebraMap F E))] : rootSet p p.SplittingField ≃ rootSet p E :=
  Equiv.ofBijective (mapRoots p E) (mapRoots_bijective p E)

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