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. -/