R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1276068
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ ¬↑(finSuccEquiv R n) f = 0
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1276068
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ Finset.Nonempty (Polynomial.support (↑(finSuccEquiv R n) f))
simp only [Finset.nonempty_iff_ne_empty, Ne, Polynomial.support_eq_empty]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1276068
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
⊢ f = 0
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1276068
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ ¬↑(finSuccEquiv R n) f = 0
refine fun c => h ?_
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1276068
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ f = 0
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1276068
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
⊢ f = 0
let ii := (finSuccEquiv R n).symm
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1276068
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ f = 0
calc
  f = ii (finSuccEquiv R n f) := by
    simpa only [← AlgEquiv.invFun_eq_symm] using ((finSuccEquiv R n).left_inv f).symm
  _ = ii 0 := by rw [c]
  _ = 0 := by simp
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1276068
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ f = ↑ii (↑(finSuccEquiv R n) f)
simpa only [← AlgEquiv.invFun_eq_symm] using ((finSuccEquiv R n).left_inv f).symm
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1276068
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ ↑ii (↑(finSuccEquiv R n) f) = ↑ii 0
rw [c]
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1276068
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
c : ↑(finSuccEquiv R n) f = 0
ii : (MvPolynomial (Fin n) R)[X] ≃ₐ[R] MvPolynomial (Fin (n + 1)) R := AlgEquiv.symm (finSuccEquiv R n)
⊢ ↑ii 0 = 0
simp