letI := Fact.mk hp
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 : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
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 : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this : Fact (↑p).Prime := { out := hp }
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R