English
Same as above: from iIsOrtho and non-vanishing diagonal terms, the family is linearly independent.
Русский
То же самое: из iIsOrtho и ненулевых диагональных членов следует линейная независимость множества векторов.
LaTeX
$$Same as above: B.iIsOrtho v ∧ ∀ i, B(v_i,v_i) ≠ 0 ⇒ LinearIndependent K v$$
Lean4
/-- The orthogonal complement of a submodule `N` with respect to some bilinear form is the set of
elements `x` which are orthogonal to all elements of `N`; i.e., for all `y` in `N`, `B y x = 0`.
Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a
chirality; in addition to this "right" orthogonal complement one could define a "left" orthogonal
complement for which, for all `y` in `N`, `B x y = 0`. This variant definition is not currently
provided in mathlib. -/
def orthogonal (B : BilinForm R M) (N : Submodule R M) : Submodule R M
where
carrier := {m | ∀ n ∈ N, IsOrtho B n m}
zero_mem' x _ := isOrtho_zero_right x
add_mem' {x y} hx hy n
hn := by rw [IsOrtho, add_right, show B n x = 0 from hx n hn, show B n y = 0 from hy n hn, zero_add]
smul_mem' c x hx n hn := by rw [IsOrtho, smul_right, show B n x = 0 from hx n hn, mul_zero]
