R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f) ↔ ∀ (n : ℕ), coeff p n ∈ Set.range ↑f
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ ∀ (n : ℕ), coeff p n ∈ Set.range ↑f
rw [lifts_iff_ringHom_rangeS, mem_map_rangeS f]
no goals
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f) ↔ ∀ (n : ℕ), coeff p n ∈ Set.range ↑f
rfl