Theorem: phi_dvd (FormalBook/Chapter_06.lean)

State before:
n : ℕ
⊢ phi n ∣ X ^ n - 1
Tactic:
rw [phi]
State after:
n : ℕ
⊢ cyclotomic n ℤ ∣ X ^ n - 1

State before:
n : ℕ
⊢ cyclotomic n ℤ ∣ X ^ n - 1
Tactic:
exact cyclotomic.dvd_X_pow_sub_one n ℤ
State after:
no goals