algebraMap_surjective — Mathlib

English

The algebra map from P.Ring to S is surjective, i.e., every element of S is the image of some polynomial expression in the generators.

Русский

Алгебраическое отображение из P.Ring в S сюръективно: каждый элемент S является образом некоторого полиномиального выражения в генераторах.

LaTeX

$$algebraMap_surjective (P) : Function.Surjective (algebraMap P.Ring S)$$

Lean4

theorem algebraMap_surjective : Function.Surjective (algebraMap P.Ring S) :=
  (⟨_, P.algebraMap_apply _ ▸ P.aeval_val_σ ·⟩)

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