lifts_iff_set_range — Mathlib

English

A polynomial p lies in lifts f if and only if p lies in the range of map f.

Русский

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

LaTeX

$$$$ p \in \mathrm{lifts}(f) \iff p \in \mathrm{Set.range}(\mathrm{map} f) $$$$

Lean4

theorem lifts_iff_set_range (p : S[X]) : p ∈ lifts f ↔ p ∈ Set.range (map f) := by
  simp only [coe_mapRingHom, lifts, Set.mem_range, RingHom.mem_rangeS]

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