erase_mem_lifts — Mathlib

English

If p lifts, then erasing the coefficient at position n, p.erase n, also lifts.

Русский

Если p поднимается, то удаление коэффициента на позиции n, p.erase n, тоже поднимается.

LaTeX

$$$ p.erase(n) \in \mathrm{lifts}\ f$$$

Lean4

/-- If `p` lifts then `p.erase n` lifts. -/
theorem erase_mem_lifts {p : S[X]} (n : ℕ) (h : p ∈ lifts f) : p.erase n ∈ lifts f :=
  by
  rw [lifts_iff_ringHom_rangeS, mem_map_rangeS] at h ⊢
  intro k
  by_cases hk : k = n
  · use 0
    simp only [hk, RingHom.map_zero, erase_same]
  obtain ⟨i, hi⟩ := h k
  use i
  simp only [hi, hk, erase_ne, Ne, not_false_iff]

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