n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ WithBot.unbot' 0 ↑(Nat.totient n) = Nat.totient n
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ natDegree (cyclotomic n R) = Nat.totient n
rw [natDegree, degree_cyclotomic]
no goals
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ WithBot.unbot' 0 ↑(Nat.totient n) = Nat.totient n
norm_cast