lifts_iff_liftsRing — Mathlib

English

If R and S are rings, p ∈ lifts f iff p ∈ liftsRing f.

Русский

Если R и S кольца, то p принадлежит lifts f тогда и только тогда, когда p принадлежит liftsRing f.

LaTeX

$$$ p \in \mathrm{lifts}(f) \leftrightarrow p \in \mathrm{liftsRing}(f) $$$

Lean4

/-- If `R` and `S` are rings, `p` is in the subring of polynomials that lift if and only if it is in
the subsemiring of polynomials that lift. -/
theorem lifts_iff_liftsRing (p : S[X]) : p ∈ lifts f ↔ p ∈ liftsRing f := by
  simp only [lifts, liftsRing, RingHom.mem_range, RingHom.mem_rangeS]

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