K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
this : Module.rank K (V ⧸ s) + Module.rank K { x // x ∈ s } = Module.rank K V
⊢ finrank K (V ⧸ s) + finrank K { x // x ∈ s } = finrank K V
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
⊢ finrank K (V ⧸ s) + finrank K { x // x ∈ s } = finrank K V
have := rank_quotient_add_rank 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
this : ↑(finrank K (V ⧸ s)) + ↑(finrank K { x // x ∈ s }) = ↑(finrank K V)
⊢ finrank K (V ⧸ s) + finrank K { x // x ∈ s } = finrank K V
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
this : Module.rank K (V ⧸ s) + Module.rank K { x // x ∈ s } = Module.rank K V
⊢ finrank K (V ⧸ s) + finrank K { x // x ∈ s } = finrank K V
rw [← finrank_eq_rank, ← finrank_eq_rank, ← finrank_eq_rank] at this
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
this : ↑(finrank K (V ⧸ s)) + ↑(finrank K { x // x ∈ s }) = ↑(finrank K V)
⊢ finrank K (V ⧸ s) + finrank K { x // x ∈ s } = finrank K V
exact_mod_cast this