isUnit_iff_isUnit_map — Mathlib

English

Let p ∈ R[X] satisfy p.IsPrimitive. Then p is a unit in R[X] if and only if its image under algebraMap R K is a unit in K[X], provided K is a field containing R suitably (i.e., via an algebra structure and fraction construction).

Русский

Пусть p ∈ R[X] примитивен. Тогда p единица в R[X] тогда и только тогда, когда образ algebraMap R K (p) является единицей в K[X].

LaTeX

$$$\\text{IsUnit}(p) \\iff \\text{IsUnit}(p.map (\\text{algebraMap } R K))$$$

Lean4

theorem isUnit_iff_isUnit_map {p : R[X]} (hp : p.IsPrimitive) : IsUnit p ↔ IsUnit (p.map (algebraMap R K)) :=
  hp.isUnit_iff_isUnit_map_of_injective (IsFractionRing.injective _ _)

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