base_mul_mem_lifts — Mathlib

English

If p is a polynomial in S[X] that lifts via f and r ∈ R, then the product C(f(r)) · p also lifts via f.

Русский

Если p — многочлен в S[X], поднимающийся через f, и r ∈ R, тогда произведение C(f(r)) · p тоже поднимается через f.

LaTeX

$$$ C(f(r)) \cdot p \in \mathrm{lifts}\ f$$$

Lean4

/-- If `p` lifts and `(r : R)` then `r * p` lifts. -/
theorem base_mul_mem_lifts {p : S[X]} (r : R) (hp : p ∈ lifts f) : C (f r) * p ∈ lifts f :=
  by
  simp only [lifts, RingHom.mem_rangeS] at hp ⊢
  obtain ⟨p₁, rfl⟩ := hp
  use C r * p₁
  simp only [coe_mapRingHom, map_C, map_mul]

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