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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ M (↑(monomial s) a)
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
⊢ ∀ (s : σ →₀ ℕ) (a : R), M (↑(monomial s) a)
intro s a
case h0
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ M (↑(monomial 0) a)

case ha
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    ¬a_1 ∈ f.support → b ≠ 0 → M (↑(monomial f) a) → M (↑(monomial (Finsupp.single a_1 b + f)) a)
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ M (↑(monomial s) a)
apply @Finsupp.induction σ ℕ _ _ s
case h0
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ M (↑(monomial 0) a)
case h0
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ M (↑(monomial 0) a)
show M (monomial 0 a)
no goals
case h0
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ M (↑(monomial 0) a)
exact h_C a
case ha
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : ¬n ∈ p.support
_he : e ≠ 0
ih : M (↑(monomial p) a)
⊢ M (↑(monomial (Finsupp.single n e + p)) a)
case ha
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    ¬a_1 ∈ f.support → b ≠ 0 → M (↑(monomial f) a) → M (↑(monomial (Finsupp.single a_1 b + f)) a)
intro n e p _hpn _he ih
case ha
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : ¬n ∈ p.support
_he : e ≠ 0
ih : M (↑(monomial p) a)
this : ∀ (e : ℕ), M (↑(monomial p) a * X n ^ e)
⊢ M (↑(monomial (Finsupp.single n e + p)) a)
case ha
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : ¬n ∈ p.support
_he : e ≠ 0
ih : M (↑(monomial p) a)
⊢ M (↑(monomial (Finsupp.single n e + p)) a)
have : ∀ e : ℕ, M (monomial p a * X n ^ e) := by
  intro e
  induction e with
  | zero => simp [ih]
  | succ e e_ih => simp [ih, pow_succ', (mul_assoc _ _ _).symm, h_X, e_ih]
no goals
case ha
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : ¬n ∈ p.support
_he : e ≠ 0
ih : M (↑(monomial p) a)
this : ∀ (e : ℕ), M (↑(monomial p) a * X n ^ e)
⊢ M (↑(monomial (Finsupp.single n e + p)) a)
simp [add_comm, monomial_add_single, this]
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e✝ : ℕ
p : σ →₀ ℕ
_hpn : ¬n ∈ p.support
_he : e✝ ≠ 0
ih : M (↑(monomial p) a)
e : ℕ
⊢ M (↑(monomial p) a * X n ^ e)
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : ¬n ∈ p.support
_he : e ≠ 0
ih : M (↑(monomial p) a)
⊢ ∀ (e : ℕ), M (↑(monomial p) a * X n ^ e)
intro e
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e✝ : ℕ
p : σ →₀ ℕ
_hpn : ¬n ∈ p.support
_he : e✝ ≠ 0
ih : M (↑(monomial p) a)
e : ℕ
⊢ M (↑(monomial p) a * X n ^ e)
induction e with
| zero => simp [ih]
| succ e e_ih => simp [ih, pow_succ', (mul_assoc _ _ _).symm, h_X, e_ih]
no goals
case zero
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : ¬n ∈ p.support
_he : e ≠ 0
ih : M (↑(monomial p) a)
⊢ M (↑(monomial p) a * X n ^ Nat.zero)
simp [ih]
no goals
case succ
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
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (↑C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e✝ : ℕ
p : σ →₀ ℕ
_hpn : ¬n ∈ p.support
_he : e✝ ≠ 0
ih : M (↑(monomial p) a)
e : ℕ
e_ih : M (↑(monomial p) a * X n ^ e)
⊢ M (↑(monomial p) a * X n ^ Nat.succ e)
simp [ih, pow_succ', (mul_assoc _ _ _).symm, h_X, e_ih]