R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
⊢ leadingCoeff (p * ↑C b) = 1
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
⊢ Monic (p * ↑C b)
unfold Monic
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
✝ : Nontrivial R
⊢ leadingCoeff (p * ↑C b) = 1
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
⊢ leadingCoeff (p * ↑C b) = 1
nontriviality
no goals
R : Type u
S : Type v
a b✝ : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
b : R
hp : leadingCoeff p * b = 1
✝ : Nontrivial R
⊢ leadingCoeff (p * ↑C b) = 1
rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]