lifts_iff_ringHom_rangeS — Mathlib

English

A polynomial p lies in lifts f exactly when p lies in the rangeS of mapRingHom f.

Русский

Полином p принадлежит lifts f тогда и только тогда, когда p лежит в rangeS mapRingHom f.

LaTeX

$$$$ p \in \mathrm{lifts}(f) \iff p \in (\mathrm{mapRingHom} f).\mathrm{rangeS} $$$$

Lean4

theorem lifts_iff_ringHom_rangeS (p : S[X]) : p ∈ lifts f ↔ p ∈ (mapRingHom f).rangeS := by
  simp only [coe_mapRingHom, lifts, RingHom.mem_rangeS]

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