lifts — Mathlib

English

The subsemiring lifts f consists exactly of polynomials whose coefficients come from the image of f.

Русский

Подполином lifts f состоит ровно из полиномов коэффициенты которых лежат в образе f.

LaTeX

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

Lean4

/-- We define the subsemiring of polynomials that lifts as the image of `RingHom.of (map f)`. -/
def lifts (f : R →+* S) : Subsemiring S[X] :=
  RingHom.rangeS (mapRingHom f)

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