K : Type u
V : Type v
F : Type u_2
E : Type u_1
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ Module.rank F { x // x ∈ span F {1} } = 1
K : Type u
V : Type v
F : Type u_2
E : Type u_1
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
⊢ Module.rank F { x // x ∈ span F {1} } = 1
letI := Module.nontrivial F E
K : Type u
V : Type v
F : Type u_2
E : Type u_1
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ (#↑{1}) = 1

K : Type u
V : Type v
F : Type u_2
E : Type u_1
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ LinearIndependent F fun x => ↑x
K : Type u
V : Type v
F : Type u_2
E : Type u_1
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ Module.rank F { x // x ∈ span F {1} } = 1
rw [rank_span_set]
no goals
K : Type u
V : Type v
F : Type u_2
E : Type u_1
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ (#↑{1}) = 1

K : Type u
V : Type v
F : Type u_2
E : Type u_1
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ LinearIndependent F fun x => ↑x
exacts [mk_singleton _, linearIndependent_singleton one_ne_zero]