Theorem: phi_div_2 (FormalBook/Chapter_06.lean)

State before:
n k : ℕ
x✝ : 1 ≠ k
h₂ : k ∣ n
h₃ : k < n
⊢ (X ^ k - 1) * phi n ∣ X ^ n - 1
Tactic:
have h_proper_div : k ∈ n.properDivisors := Nat.mem_properDivisors.mpr ⟨h₂, h₃⟩
State after:
n k : ℕ
x✝ : 1 ≠ k
h₂ : k ∣ n
h₃ : k < n
h_proper_div : k ∈ n.properDivisors
⊢ (X ^ k - 1) * phi n ∣ X ^ n - 1

State before:
n k : ℕ
x✝ : 1 ≠ k
h₂ : k ∣ n
h₃ : k < n
h_proper_div : k ∈ n.properDivisors
⊢ (X ^ k - 1) * phi n ∣ X ^ n - 1
Tactic:
exact X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd ℤ h_proper_div
State after:
no goals