doc: add missing LaTeX markers in docstrings

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: kim-em

Mathlib/GroupTheory/Artin/Braid.lean

@@ -16,22 +16,22 @@ This file defines the braid groups as Artin groups of type A.
 
 ## Main definitions
 
-* `BraidGroup`: The braid group B_n on n strands.
-* `BraidGroup.σ`: The standard Artin generators σ_i of the braid group.
-* `BraidGroup.toPermHom`: The canonical surjection from B_n to S_n.
+* `BraidGroup`: The braid group $B_n$ on $n$ strands.
+* `BraidGroup.σ`: The standard Artin generators $σ_i$ of the braid group.
+* `BraidGroup.toPermHom`: The canonical surjection from $B_n$ to $S_n$.
 
 ## Overview
 
-The braid group `B_n` is the group with presentation:
-* Generators: σ_1, ..., σ_{n-1}
+The braid group $B_n$ is the group with presentation:
+* Generators: $σ_1, \ldots, σ_{n-1}$
 * Relations:
-  - σ_i σ_j = σ_j σ_i for |i - j| ≥ 2 (far commutativity)
-  - σ_i σ_{i+1} σ_i = σ_{i+1} σ_i σ_{i+1} (braid relation)
+  - $σ_i σ_j = σ_j σ_i$ for $|i - j| ≥ 2$ (far commutativity)
+  - $σ_i σ_{i+1} σ_i = σ_{i+1} σ_i σ_{i+1}$ (braid relation)
 
-This is the Artin group associated to the Coxeter matrix of type A_{n-1}.
+This is the Artin group associated to the Coxeter matrix of type $A_{n-1}$.
 
-There is a canonical surjection from `B_n` to the symmetric group `S_n` sending σ_i to
-the adjacent transposition (i, i+1).
+There is a canonical surjection from $B_n$ to the symmetric group $S_n$ sending $σ_i$ to
+the adjacent transposition $(i, i+1)$.
 
 ## Next steps
 
@@ -55,7 +55,7 @@ open Equiv Fin
 
 /-! ### The braid group -/
 
-/-- The braid group `B_n` on `n` strands. This is the Artin group of type A_{n-1}. -/
+/-- The braid group `B_n` on `n` strands. This is the Artin group of type $A_{n-1}$. -/
 def BraidGroup : ℕ → Type
 | 0 => Unit
 | n + 1 => (CoxeterMatrix.Aₙ n).ArtinGroup
@@ -69,8 +69,8 @@ instance : Group (BraidGroup n) :=
   | 0 => inferInstanceAs (Group Unit)
   | n + 1 => inferInstanceAs (Group (CoxeterMatrix.Aₙ n).ArtinGroup)
 
-/-- The i-th standard Artin generator σ_i of the braid group B_n.
-This corresponds to crossing strand i over strand i+1. -/
+/-- The $i$-th standard Artin generator $σ_i$ of the braid group $B_n$.
+This corresponds to crossing strand $i$ over strand $i+1$. -/
 def σ (i : Fin n) : BraidGroup (n + 1) :=
   (CoxeterMatrix.Aₙ n).artinGenerator i
 
@@ -80,8 +80,8 @@ end BraidGroup
 
 namespace BraidGroup
 
-/-- The canonical surjection from the braid group B_{n+1} to the symmetric group S_{n+1},
-sending σ_i to the adjacent transposition (i, i+1).
+/-- The canonical surjection from the braid group $B_{n+1}$ to the symmetric group $S_{n+1}$,
+sending $σ_i$ to the adjacent transposition $(i, i+1)$.
 
 This is defined as the composition of `artinToCoxeter` and `typeAₙToPermHom`. -/
 def toPermHom (n : ℕ) : BraidGroup n →* Perm (Fin n) :=
@@ -100,7 +100,7 @@ theorem toPermHom_σ (n : ℕ) (i : Fin n) :
   rw [MonoidHom.coe_comp, Function.comp_apply]
   exact CoxeterMatrix.typeAₙToPermHom_simple _ _
 
-/-- The surjection from B_{n+1} to S_{n+1} is surjective. -/
+/-- The surjection from $B_{n+1}$ to $S_{n+1}$ is surjective. -/
 theorem toPermHom_surjective (n : ℕ) : Function.Surjective (toPermHom n) :=
   match n with
   | 0 => Function.surjective_to_subsingleton ⇑(toPermHom 0)
@@ -109,16 +109,16 @@ theorem toPermHom_surjective (n : ℕ) : Function.Surjective (toPermHom n) :=
 
 /-! ### Small braid groups -/
 
-/-- The braid group B_0 is trivial (no generators). -/
+/-- The braid group $B_0$ is trivial (no generators). -/
 instance : Unique (BraidGroup 0) :=
   inferInstanceAs (Unique Unit)
 
-/-- The braid group B_1 is trivial (no generators). -/
+/-- The braid group $B_1$ is trivial (no generators). -/
 instance : Unique (BraidGroup 1) :=
   inferInstanceAs (Unique (CoxeterMatrix.Aₙ 0).ArtinGroup)
 
 /-- The Artin relations for `Aₙ 1` are all trivial.
-When i = j, the relation is `of i * (of i)⁻¹ = 1`. -/
+When $i = j$, the relation is `of i * (of i)⁻¹ = 1`. -/
 theorem artinRelationsSet_Aₙ_one_eq_one :
     (CoxeterMatrix.Aₙ 1).artinRelationsSet = {1} := by
   ext r
@@ -135,8 +135,8 @@ theorem artinRelationsSet_Aₙ_one_eq_one :
     simp only [CoxeterMatrix.artinRelation, CoxeterMatrix.diagonal,
       CoxeterSystem.alternatingWord, mul_inv_cancel, hr]
 
-/-- The braid group B_2 is isomorphic to ℤ (one generator, no non-trivial relations).
-The isomorphism sends the unique generator σ_0 to 1 ∈ ℤ. -/
+/-- The braid group $B_2$ is isomorphic to $ℤ$ (one generator, no non-trivial relations).
+The isomorphism sends the unique generator $σ_0$ to $1 ∈ ℤ$. -/
 def braidGroupTwoEquivInt : BraidGroup 2 ≃* Multiplicative ℤ := by
   -- BraidGroup 2 = (Aₙ 1).ArtinGroup = PresentedGroup (Aₙ 1).artinRelationsSet
   -- The relations are all trivial, so this equals FreeGroup (Fin 1) / ⊥ ≃ FreeGroup (Fin 1)
@@ -150,7 +150,7 @@ def braidGroupTwoEquivInt : BraidGroup 2 ≃* Multiplicative ℤ := by
       ((FreeGroup.freeGroupCongr (Equiv.equivPUnit (Fin 1))).trans
         FreeGroup.freeGroupUnitMulEquivInt))
 
-/-- The generator σ_0 of B_2 maps to 1 under the isomorphism with ℤ. -/
+/-- The generator $σ_0$ of $B_2$ maps to $1$ under the isomorphism with $ℤ$. -/
 @[simp]
 theorem braidGroupTwoEquivInt_σ :
     braidGroupTwoEquivInt (σ 0) = Multiplicative.ofAdd 1 := by