fix(data/mv_polynomial): fix doc strings (#4219)

src/data/mv_polynomial/basic.lean

@@ -125,7 +125,7 @@ variables (R σ)
 theorem algebra_map_eq : algebra_map R (mv_polynomial σ R) = C := rfl
 variables {R σ}
 
-/-- `X n` is the degree `1` monomial `1*n` -/
+/-- `X n` is the degree `1` monomial $X_n$. -/
 def X (n : σ) : mv_polynomial σ R := monomial (single n 1) 1
 
 @[simp] lemma C_0 : C 0 = (0 : mv_polynomial σ R) := by simp [C, monomial]; refl

src/data/mv_polynomial/comap.lean

@@ -16,7 +16,7 @@ This file defines the `comap` function on `mv_polynomial`.
 
 ## Notation
 
-As in other polynomial files we typically use the notation:
+As in other polynomial files, we typically use the notation:
 
 + `σ : Type*` (indexing the variables)
 

src/data/mv_polynomial/comm_ring.lean

@@ -16,7 +16,7 @@ This file does not define any new operations, but proves some of these stronger
 
 ## Notation
 
-As in other polynomial files we typically use the notation:
+As in other polynomial files, we typically use the notation:
 
 + `σ : Type*` (indexing the variables)
 

src/data/mv_polynomial/equiv.lean

@@ -15,7 +15,7 @@ based on equivalences between the underlying types.
 
 ## Notation
 
-As in other polynomial files we typically use the notation:
+As in other polynomial files, we typically use the notation:
 
 + `σ : Type*` (indexing the variables)
 

src/data/mv_polynomial/pderivative.lean

@@ -22,7 +22,7 @@ It is based purely on the polynomial exponents and coefficients.
 
 ## Notation
 
-This file uses notation slightly different from other `mv_polynomial` files:
+As in other polynomial files, we typically use the notation:
 
 + `σ : Type*` (indexing the variables)
 

src/data/mv_polynomial/rename.lean

@@ -18,7 +18,7 @@ which modifies the set of variables.
 
 ## Notation
 
-As in other polynomial files we typically use the notation:
+As in other polynomial files, we typically use the notation:
 
 + `σ τ α : Type*` (indexing the variables)
 

src/data/mv_polynomial/variables.lean

@@ -36,7 +36,7 @@ monomial of $P$.
 
 ## Notation
 
-As in other polynomial files we typically use the notation:
+As in other polynomial files, we typically use the notation:
 
 + `σ : Type*` (indexing the variables)