Theorem: CyclotomicIntegers.powerBasis_dim (FltRegular/NumberTheory/CyclotomicRing.lean)

State before:
p : ℕ
hpri : Fact p.Prime
⊢ (powerBasis p).dim = p - 1
Tactic:
simp [powerBasis, Nat.totient_prime hpri.out, natDegree_cyclotomic]
State after:
no goals