F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
⊢ Separable (X ^ n - 1) → ↑n ≠ 0
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
⊢ Separable (X ^ n - 1) ↔ ↑n ≠ 0
refine' ⟨_, fun h => separable_X_pow_sub_C_unit 1 (IsUnit.mk0 (↑n) h)⟩
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
⊢ (∃ a b, a * (X ^ n - 1) + b * (↑C ↑n * X ^ (n - 1)) = 1) → ↑n ≠ 0
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
⊢ Separable (X ^ n - 1) → ↑n ≠ 0
rw [separable_def', derivative_sub, derivative_X_pow, derivative_one, sub_zero]
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
h : IsCoprime (X ^ n - 1) (↑C ↑n * X ^ (n - 1))
hn' : ↑n = 0
⊢ False
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
⊢ (∃ a b, a * (X ^ n - 1) + b * (↑C ↑n * X ^ (n - 1)) = 1) → ↑n ≠ 0
rintro (h : IsCoprime _ _) hn'
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
h : IsUnit (X ^ n - 1)
hn' : ↑n = 0
⊢ False
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
h : IsCoprime (X ^ n - 1) (↑C ↑n * X ^ (n - 1))
hn' : ↑n = 0
⊢ False
rw [hn', C_0, MulZeroClass.zero_mul, isCoprime_zero_right] at h
no goals
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
n : ℕ
h : IsUnit (X ^ n - 1)
hn' : ↑n = 0
⊢ False
exact not_isUnit_X_pow_sub_one F n h