injective — Mathlib

English

The natural bijection between AdjoinRoot(minpoly x) and adjoin x exists when x is integral.

Русский

Существует биекция между AdjoinRoot(minpoly x) и adjoin x при интегральности x.

LaTeX

$$$minpoly.ToAdjoin.injective\land minpoly.ToAdjoin.surjective$$$

Lean4

theorem injective (hx : IsIntegral R x) : Function.Injective (Minpoly.toAdjoin R x) :=
  by
  refine (injective_iff_map_eq_zero _).2 fun P₁ hP₁ => ?_
  obtain ⟨P, rfl⟩ := mk_surjective P₁
  simp_all [← Subalgebra.coe_eq_zero, isIntegrallyClosed_dvd_iff hx]

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