R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
⊢ natDegree (∏ i in s, f i) = ∑ i in s, natDegree (f i)
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
⊢ natDegree (∏ i in s, f i) = ∑ i in s, natDegree (f i)
nontriviality R
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
⊢ ∏ i in s, leadingCoeff (f i) ≠ 0
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
⊢ natDegree (∏ i in s, f i) = ∑ i in s, natDegree (f i)
apply natDegree_prod'
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
⊢ ∀ (a : ι), a ∈ s → leadingCoeff (f a) ≠ 0
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
⊢ ∏ i in s, leadingCoeff (f i) ≠ 0
rw [prod_ne_zero_iff]
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
x : ι
hx : x ∈ s
⊢ leadingCoeff (f x) ≠ 0
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
⊢ ∀ (a : ι), a ∈ s → leadingCoeff (f a) ≠ 0
intro x hx
no goals
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
t : Multiset R[X]
h : ∀ (i : ι), i ∈ s → f i ≠ 0
✝ : Nontrivial R
x : ι
hx : x ∈ s
⊢ leadingCoeff (f x) ≠ 0
simp [h x hx]