case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
hq : Monic q
u : R[X]ˣ
hu : p * ↑u = q
⊢ p = q
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
hq : Monic q
hpq : Associated p q
⊢ p = q
obtain ⟨u, hu⟩ := hpq
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : leadingCoeff p = 1
hq : leadingCoeff q = 1
u : R[X]ˣ
hu : p * ↑u = q
⊢ p = q
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
hq : Monic q
u : R[X]ˣ
hu : p * ↑u = q
⊢ p = q
unfold Monic at hp hq
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : leadingCoeff p = 1
hq : leadingCoeff q = 1
u : R[X]ˣ
hu : p * ↑C (coeff (↑u) 0) = q
⊢ p = q
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : leadingCoeff p = 1
hq : leadingCoeff q = 1
u : R[X]ˣ
hu : p * ↑u = q
⊢ p = q
rw [eq_C_of_degree_le_zero (degree_coe_units _).le] at hu
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : leadingCoeff p = 1
u : R[X]ˣ
hq : coeff (↑u) 0 = 1
hu : p * ↑C (coeff (↑u) 0) = q
⊢ p = q
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : leadingCoeff p = 1
hq : leadingCoeff q = 1
u : R[X]ˣ
hu : p * ↑C (coeff (↑u) 0) = q
⊢ p = q
rw [← hu, leadingCoeff_mul, hp, one_mul, leadingCoeff_C] at hq
no goals
case intro
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : leadingCoeff p = 1
u : R[X]ˣ
hq : coeff (↑u) 0 = 1
hu : p * ↑C (coeff (↑u) 0) = q
⊢ p = q
rwa [hq, C_1, mul_one] at hu