R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
p q : MvPolynomial σ R
h : ↑(map f) p = ↑(map f) q
⊢ p = q
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
⊢ Injective ↑(map f)
intro p q h
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), ↑f (coeff m p) = ↑f (coeff m q)
⊢ ∀ (m : σ →₀ ℕ), coeff m p = coeff m q
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
p q : MvPolynomial σ R
h : ↑(map f) p = ↑(map f) q
⊢ p = q
simp only [ext_iff, coeff_map] at h⊢
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), ↑f (coeff m p) = ↑f (coeff m q)
m : σ →₀ ℕ
⊢ coeff m p = coeff m q
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), ↑f (coeff m p) = ↑f (coeff m q)
⊢ ∀ (m : σ →₀ ℕ), coeff m p = coeff m q
intro m
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ q✝ : MvPolynomial σ R
f : R →+* S₁
hf : Injective ↑f
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), ↑f (coeff m p) = ↑f (coeff m q)
m : σ →₀ ℕ
⊢ coeff m p = coeff m q
exact hf (h m)