case mp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ RingHom.rangeS (mapRingHom f) → ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f

case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f) → p ∈ RingHom.rangeS (mapRingHom f)
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ RingHom.rangeS (mapRingHom f) ↔ ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
constructor
case mp.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ coeff (↑(mapRingHom f) p) n ∈ RingHom.rangeS f
case mp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ RingHom.rangeS (mapRingHom f) → ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
rintro ⟨p, rfl⟩ n
case mp.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ ↑f (coeff p n) ∈ RingHom.rangeS f
case mp.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ coeff (↑(mapRingHom f) p) n ∈ RingHom.rangeS f
rw [coe_mapRingHom, coeff_map]
no goals
case mp.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ ↑f (coeff p n) ∈ RingHom.rangeS f
exact Set.mem_range_self _
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ p ∈ RingHom.rangeS (mapRingHom f)
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f) → p ∈ RingHom.rangeS (mapRingHom f)
intro h
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ ∑ i in range (natDegree p + 1), ↑C (coeff p i) * X ^ i ∈ RingHom.rangeS (mapRingHom f)
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ p ∈ RingHom.rangeS (mapRingHom f)
rw [p.as_sum_range_C_mul_X_pow]
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ ∀ (c : ℕ), c ∈ range (natDegree p + 1) → ↑C (coeff p c) * X ^ c ∈ RingHom.rangeS (mapRingHom f)
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ ∑ i in range (natDegree p + 1), ↑C (coeff p i) * X ^ i ∈ RingHom.rangeS (mapRingHom f)
refine' (mapRingHom f).rangeS.sum_mem _
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
i : ℕ
_hi : i ∈ range (natDegree p + 1)
⊢ ↑C (coeff p i) * X ^ i ∈ RingHom.rangeS (mapRingHom f)
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ ∀ (c : ℕ), c ∈ range (natDegree p + 1) → ↑C (coeff p c) * X ^ c ∈ RingHom.rangeS (mapRingHom f)
intro i _hi
case mpr.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
i : ℕ
_hi : i ∈ range (natDegree p + 1)
c : R
hc : ↑f c = coeff p i
⊢ ↑C (coeff p i) * X ^ i ∈ RingHom.rangeS (mapRingHom f)
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
i : ℕ
_hi : i ∈ range (natDegree p + 1)
⊢ ↑C (coeff p i) * X ^ i ∈ RingHom.rangeS (mapRingHom f)
rcases h i with ⟨c, hc⟩
case mpr.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
i : ℕ
_hi : i ∈ range (natDegree p + 1)
c : R
hc : ↑f c = coeff p i
⊢ ↑(mapRingHom f) (↑C c * X ^ i) = ↑C (coeff p i) * X ^ i
case mpr.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
i : ℕ
_hi : i ∈ range (natDegree p + 1)
c : R
hc : ↑f c = coeff p i
⊢ ↑C (coeff p i) * X ^ i ∈ RingHom.rangeS (mapRingHom f)
use C c * X ^ i
no goals
case mpr.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
i : ℕ
_hi : i ∈ range (natDegree p + 1)
c : R
hc : ↑f c = coeff p i
⊢ ↑(mapRingHom f) (↑C c * X ^ i) = ↑C (coeff p i) * X ^ i
rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]