R : Type ?u.260339
R₁ : Type ?u.260342
R₂ : Type ?u.260345
R₃ : Type ?u.260348
M : Type ?u.260351
M₁ : Type ?u.260354
M₂ : Type ?u.260357
Mₗ₁ : Type ?u.260360
Mₗ₁' : Type ?u.260363
Mₗ₂ : Type ?u.260366
Mₗ₂' : Type ?u.260369
K : Type u_1
K₁ : Type ?u.260375
K₂ : Type ?u.260378
V : Type u_2
V₁ : Type ?u.260384
V₂ : Type ?u.260387
n : Type ?u.260390
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K {x} ⊔ ker (↑B x) = ⊤
R : Type ?u.260339
R₁ : Type ?u.260342
R₂ : Type ?u.260345
R₃ : Type ?u.260348
M : Type ?u.260351
M₁ : Type ?u.260354
M₂ : Type ?u.260357
Mₗ₁ : Type ?u.260360
Mₗ₁' : Type ?u.260363
Mₗ₂ : Type ?u.260366
Mₗ₂' : Type ?u.260369
K : Type u_1
K₁ : Type ?u.260375
K₂ : Type ?u.260378
V : Type u_2
V₁ : Type ?u.260384
V₂ : Type ?u.260387
n : Type ?u.260390
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K {x} ⊔ Submodule.orthogonalBilin (Submodule.span K {x}) B = ⊤
rw [orthogonal_span_singleton_eq_to_lin_ker]
no goals
R : Type ?u.260339
R₁ : Type ?u.260342
R₂ : Type ?u.260345
R₃ : Type ?u.260348
M : Type ?u.260351
M₁ : Type ?u.260354
M₂ : Type ?u.260357
Mₗ₁ : Type ?u.260360
Mₗ₁' : Type ?u.260363
Mₗ₂ : Type ?u.260366
Mₗ₂' : Type ?u.260369
K : Type u_1
K₁ : Type ?u.260375
K₂ : Type ?u.260378
V : Type u_2
V₁ : Type ?u.260384
V₂ : Type ?u.260387
n : Type ?u.260390
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
J : K →+* K
J₁ J₁' : K₁ →+* K
B : V →ₗ[K] V →ₗ[K] K
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K {x} ⊔ ker (↑B x) = ⊤
exact (B x).span_singleton_sup_ker_eq_top hx