R : Type ?u.1321214
M : Type ?u.1321217
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1321253
M₁ : Type ?u.1321256
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1321865
M₂ : Type ?u.1321868
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1322055
M₃ : Type ?u.1322058
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K {x} ⊔ LinearMap.ker (↑(↑toLin B) x) = ⊤
R : Type ?u.1321214
M : Type ?u.1321217
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1321253
M₁ : Type ?u.1321256
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1321865
M₂ : Type ?u.1321868
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1322055
M₃ : Type ?u.1322058
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K {x} ⊔ orthogonal B (Submodule.span K {x}) = ⊤
rw [orthogonal_span_singleton_eq_toLin_ker]
no goals
R : Type ?u.1321214
M : Type ?u.1321217
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.1321253
M₁ : Type ?u.1321256
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.1321865
M₂ : Type ?u.1321868
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.1322055
M₃ : Type ?u.1322058
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
N L : Submodule R M
B : BilinForm K V
x : V
hx : ¬IsOrtho B x x
⊢ Submodule.span K {x} ⊔ LinearMap.ker (↑(↑toLin B) x) = ⊤
exact LinearMap.span_singleton_sup_ker_eq_top _ hx