no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.681610
⊢ leadingCoeff p ^ Nat.zero ≠ 0 → leadingCoeff (p ^ Nat.zero) = leadingCoeff p ^ Nat.zero
simp
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.681610
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
⊢ leadingCoeff (p ^ Nat.succ n) = leadingCoeff p ^ Nat.succ n
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.681610
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
⊢ leadingCoeff (p ^ Nat.succ n) = leadingCoeff p ^ Nat.succ n
have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, mul_zero]
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.681610
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0
⊢ leadingCoeff (p ^ Nat.succ n) = leadingCoeff p ^ Nat.succ n
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.681610
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
⊢ leadingCoeff (p ^ Nat.succ n) = leadingCoeff p ^ Nat.succ n
have h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0 := by rwa [pow_succ, ← ih h₁] at h
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.681610
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0
⊢ leadingCoeff (p ^ Nat.succ n) = leadingCoeff p ^ Nat.succ n
rw [pow_succ, pow_succ, leadingCoeff_mul' h₂, ih h₁]
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.681610
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
h₁ : leadingCoeff p ^ n = 0
⊢ leadingCoeff p ^ Nat.succ n = 0
rw [pow_succ, h₁, mul_zero]
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.681610
n : ℕ
ih : leadingCoeff p ^ n ≠ 0 → leadingCoeff (p ^ n) = leadingCoeff p ^ n
h : leadingCoeff p ^ Nat.succ n ≠ 0
h₁ : leadingCoeff p ^ n ≠ 0
⊢ leadingCoeff p * leadingCoeff (p ^ n) ≠ 0
rwa [pow_succ, ← ih h₁] at h