algEquivSplittingFieldAux — Mathlib

English

There is an algebra isomorphism between the splitting field of f and SplittingFieldAux f.natDegree f.

Русский

Между разворачивающим полем f и SplittingFieldAux f.natDegree f существует алгебраическое изоморфизм.

LaTeX

$$$\\text{SplittingField}(f) \\cong_K \\text{SplittingFieldAux}(f.natDegree, f)$$$

Lean4

/-- The algebra equivalence with `SplittingFieldAux`,
which we will use to construct the field structure. -/
def algEquivSplittingFieldAux (f : K[X]) : SplittingField f ≃ₐ[K] SplittingFieldAux f.natDegree f :=
  Ideal.quotientKerAlgEquivOfSurjective fun x => ⟨MvPolynomial.X x, by simp⟩

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