K : Type u
V : Type v
F : Type u_2
E : Type u_1
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F { x // x ∈ ↑Subalgebra.toSubmodule ⊤ }
K : Type u
V : Type v
F : Type u_2
E : Type u_1
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F { x // x ∈ ⊤ }
rw [← Algebra.top_toSubmodule]
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
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F { x // x ∈ ↑Subalgebra.toSubmodule ⊤ }
rfl