surjective — Mathlib

English

For any x ∈ S, the map Minpoly.toAdjoin R x is surjective onto the subalgebra adjoin R({x}).

Русский

Любое элемент подалгебры $\operatorname{adjoin}_R(\\{x\\})$ является образом отображения Minpoly.toAdjoin R x.

LaTeX

$$∀ y ∈ \\operatorname{adjoin}_R(\\{x\\}), ∃ z ∈ \\operatorname{AdjoinRoot}(\\minpoly_R(x)) с \\; (\\operatorname{Minpoly.toAdjoin} \\, R \\, x) \\, z = y.$$

Lean4

theorem surjective : Function.Surjective (Minpoly.toAdjoin R x) :=
  by
  rw [← AlgHom.range_eq_top, _root_.eq_top_iff, ← adjoin_adjoin_coe_preimage]
  exact adjoin_le fun ⟨y₁, y₂⟩ h ↦ ⟨mk (minpoly R x) X, by simpa using h.symm⟩

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