R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ IsUnit q
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hq : ¬IsUnit q
hsep : Separable p
⊢ multiplicity q p ≤ 1
contrapose! hq
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ q * q ∣ p
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ IsUnit q
apply isUnit_of_self_mul_dvd_separable hsep
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ q ^ 2 ∣ p
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ q * q ∣ p
rw [← sq]
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ ↑2 ≤ multiplicity q p
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ q ^ 2 ∣ p
apply multiplicity.pow_dvd_of_le_multiplicity
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
h : { Dom := 1.Dom ∧ 1.Dom, get := fun x => 2 } ≤ multiplicity q p
⊢ ↑2 ≤ multiplicity q p
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
⊢ ↑2 ≤ multiplicity q p
have h : ⟨Part.Dom 1 ∧ Part.Dom 1, fun _ ↦ 2⟩ ≤ multiplicity q p := PartENat.add_one_le_of_lt hq
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
h : { Dom := 1.Dom, get := fun x => 2 } ≤ multiplicity q p
⊢ ↑2 ≤ multiplicity q p
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
h : { Dom := 1.Dom ∧ 1.Dom, get := fun x => 2 } ≤ multiplicity q p
⊢ ↑2 ≤ multiplicity q p
rw [and_self] at h
no goals
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ : ℕ
p q : R[X]
hsep : Separable p
hq : 1 < multiplicity q p
h : { Dom := 1.Dom, get := fun x => 2 } ≤ multiplicity q p
⊢ ↑2 ≤ multiplicity q p
exact h