chore(linear_algebra/quadratic_form): make Sylvester's law of inertia…

… bold in the doc string (#8610)
leanprover-community · Aug 10, 2021 · 5739199 · 5739199
1 parent e2b7f70
commit 5739199
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/linear_algebra/quadratic_form.lean b/src/linear_algebra/quadratic_form.lean
@@ -978,7 +978,7 @@ begin
   apply_instance
 end
 
-/-- Sylvester's law of inertia: A nondegenerate real quadratic form is equivalent to a weighted
+/-- **Sylvester's law of inertia**: A nondegenerate real quadratic form is equivalent to a weighted
 sum of squares with the weights being ±1. -/
 theorem equivalent_one_neg_one_weighted_sum_squared
   {M : Type*} [add_comm_group M] [module ℝ M] [finite_dimensional ℝ M]