Theorem: systemOfUnits.finrank_spanA (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 : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Tactic:
classical
letI := Fact.mk hp
have := finrank_span_set_eq_card' (R := A) (Set.range f)
  ((linearIndependent_subtype_range hf.injective).mpr hf)
simp only [Set.toFinset_range, Finset.card_image_of_injective _ hf.injective, card_fin] at this
rw [← CyclotomicIntegers.powerBasis_dim, ← PowerBasis.finrank']
conv_rhs => rw [← this]
have := Module.Free.of_basis (Basis.span hf)
have := Module.Finite.of_basis (Basis.span hf)
rw [finrank_mul_finrank]
State after:
no goals

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

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 : ℕ
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
Tactic:
have := finrank_span_set_eq_card' (R := A) (Set.range f)
  ((linearIndependent_subtype_range hf.injective).mpr hf)
State after:
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 }
this :
  finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (Set.range f).toFinset.card
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R

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 : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this :
  finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (Set.range f).toFinset.card
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Tactic:
simp only [Set.toFinset_range, Finset.card_image_of_injective _ hf.injective, card_fin] at this
State after:
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 }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R

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 : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = (↑p - 1) * R
Tactic:
rw [← CyclotomicIntegers.powerBasis_dim, ← PowerBasis.finrank']
State after:
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 }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = finrank ℤ (CyclotomicIntegers ↑p) * R

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 : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = finrank ℤ (CyclotomicIntegers ↑p) * R
Tactic:
conv_rhs => rw [← this]
State after:
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 }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))

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 : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝ : Fact (↑p).Prime := { out := hp }
this : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
Tactic:
have := Module.Free.of_basis (Basis.span hf)
State after:
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 }
this✝ : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
this : Module.Free (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))

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 : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝¹ : Fact (↑p).Prime := { out := hp }
this✝ : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
this : Module.Free (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
Tactic:
have := Module.Finite.of_basis (Basis.span hf)
State after:
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 }
this✝¹ : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
this✝ : Module.Free (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
this : Module.Finite (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))

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 : ℕ
f : Fin R → G
hf : LinearIndependent (CyclotomicIntegers ↑p) f
this✝² : Fact (↑p).Prime := { out := hp }
this✝¹ : finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) = R
this✝ : Module.Free (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
this : Module.Finite (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
⊢ finrank ℤ ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    finrank ℤ (CyclotomicIntegers ↑p) *
      finrank (CyclotomicIntegers ↑p) ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range f))
Tactic:
rw [finrank_mul_finrank]
State after:
no goals