𝕜 : Type u_1
E : Type u_2
F : Type ?u.1011570
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K✝ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
n : ℕ
h_dim : finrank 𝕜 { x // x ∈ K } + n = finrank 𝕜 E
⊢ finrank 𝕜 { x // x ∈ K } + finrank 𝕜 { x // x ∈ Kᗮ } = finrank 𝕜 { x // x ∈ K } + n
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1011570
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K✝ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
n : ℕ
h_dim : finrank 𝕜 { x // x ∈ K } + n = finrank 𝕜 E
⊢ finrank 𝕜 { x // x ∈ Kᗮ } = n
rw [← add_right_inj (finrank 𝕜 K)]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1011570
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K✝ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
n : ℕ
h_dim : finrank 𝕜 { x // x ∈ K } + n = finrank 𝕜 E
⊢ finrank 𝕜 { x // x ∈ K } + finrank 𝕜 { x // x ∈ Kᗮ } = finrank 𝕜 { x // x ∈ K } + n
simp [Submodule.finrank_add_finrank_orthogonal, h_dim]