K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : finrank F { x // x ∈ S } = 1
this : FiniteDimensional F { x // x ∈ S }
⊢ Module.rank F { x // x ∈ S } ≤ 1
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : finrank F { x // x ∈ S } = 1
⊢ Module.rank F { x // x ∈ S } ≤ 1
haveI : FiniteDimensional F S := finiteDimensional_of_finrank_eq_succ h
no goals
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : finrank F { x // x ∈ S } = 1
this : FiniteDimensional F { x // x ∈ S }
⊢ Module.rank F { x // x ∈ S } ≤ 1
rw [← finrank_eq_rank, h, Nat.cast_one]