Commit 2021-04-03 03:51 9c6fe3cc

feat(linear_algebra/bilinear_form): Bilinear form restricted on a subspace is nondegenerate under some condition (#6855) The main result is restrict_nondegenerate_iff_is_compl_orthogonal which states that: a subspace is complement to its orthogonal complement with respect to some bilinear form if and only if that bilinear form restricted on to the subspace is nondegenerate. To prove this, I also introduced dual_annihilator_comap. This is a definition that allows us to treat the dual annihilator of a dual annihilator as a subspace in the original space.