From 7320fe0673eef9f72102a3195a35b940e329e17f Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Sun, 28 Jan 2024 17:46:45 +0100
Subject: [PATCH] Update CovariantAndContravariant.lean

---
 Mathlib/Algebra/CovariantAndContravariant.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/CovariantAndContravariant.lean b/Mathlib/Algebra/CovariantAndContravariant.lean
index 942eacb855158..83ad88a05c2ef 100644
--- a/Mathlib/Algebra/CovariantAndContravariant.lean
+++ b/Mathlib/Algebra/CovariantAndContravariant.lean
@@ -72,7 +72,7 @@ variable {M N : Type*} (μ : M → N → N) (r : N → N → Prop)
 
 variable (M N)
 
-/-- `Covariant` is useful to formulate succintly statements about the interactions between an
+/-- `Covariant` is useful to formulate succinctly statements about the interactions between an
 action of a Type on another one and a relation on the acted-upon Type.
 
 See the `CovariantClass` doc-string for its meaning. -/
@@ -80,7 +80,7 @@ def Covariant : Prop :=
   ∀ (m) {n₁ n₂}, r n₁ n₂ → r (μ m n₁) (μ m n₂)
 #align covariant Covariant
 
-/-- `Contravariant` is useful to formulate succintly statements about the interactions between an
+/-- `Contravariant` is useful to formulate succinctly statements about the interactions between an
 action of a Type on another one and a relation on the acted-upon Type.
 
 See the `ContravariantClass` doc-string for its meaning. -/