K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : s < ⊤
⊢ finrank K { x // x ∈ s } < finrank K { x // x ∈ s } + finrank K (V ⧸ s)
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : s < ⊤
⊢ finrank K { x // x ∈ s } < finrank K V
rw [← s.finrank_quotient_add_finrank, add_comm]
no goals
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : s < ⊤
⊢ finrank K { x // x ∈ s } < finrank K { x // x ∈ s } + finrank K (V ⧸ s)
exact Nat.lt_add_of_pos_right (finrank_pos_iff.mpr (Quotient.nontrivial_of_lt_top _ h))