Theorem: PowerBasis.finrank' (FltRegular/NumberTheory/SystemOfUnits.lean)

State before:
p : ℕ+
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : NumberField K
inst✝⁹ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁸ : Field k
inst✝⁷ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝⁶ : AddCommGroup G
r : ℕ
inst✝⁵ : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁴ : Module (CyclotomicIntegers ↑p) G
R : Type u_5
S : Type u_6
inst✝³ : CommRing R
inst✝² : Nontrivial R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pb : PowerBasis R S
⊢ finrank R S = pb.dim
Tactic:
rw [FiniteDimensional.finrank_eq_card_basis pb.basis, Fintype.card_fin]
State after:
no goals