liftsRing — Mathlib

English

The subring of polynomials that lift, liftsRing f, is equal to the range of mapRingHom f.

Русский

Подкольцо многочленов, поднимающихся через f, liftsRing f, равно образу отображения mapRingHom f.

LaTeX

$$$ \mathrm{liftsRing}(f) = \operatorname{range}(\mathrm{mapRingHom}\, f) $$$

Lean4

/-- The subring of polynomials that lift. -/
def liftsRing (f : R →+* S) : Subring S[X] :=
  RingHom.range (mapRingHom f)

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