doc(undergrad): add unitary and orthogonal group (#15456)

leanprover-community · Jul 17, 2022 · bb08977 · bb08977
1 parent fcceffa
commit bb08977
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
@@ -219,8 +219,8 @@ Bilinear and Quadratic Forms Over a Vector Space:
     norm: 'inner_product_space.of_core.to_has_norm'
     orthonormal bases: 'maximal_orthonormal_iff_basis_of_finite_dimensional'
   Endomorphisms:
-    orthogonal group: ''
-    unitary group: ''
+    orthogonal group: 'matrix.orthogonal_group'
+    unitary group: 'matrix.unitary_group'
     special orthogonal group: ''
     special unitary group: ''
     self-adjoint endomorphism: 'inner_product_space.is_self_adjoint'