doc(Order): remove some mathlib3 names in docs (#11953)

leanprover-community · Apr 6, 2024 · 7239b9f · 7239b9f
1 parent a8a6713
commit 7239b9f
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib/Order/Category/NonemptyFinLinOrd.lean b/Mathlib/Order/Category/NonemptyFinLinOrd.lean
@@ -257,7 +257,7 @@ theorem nonemptyFinLinOrd_dual_comp_forget_to_linOrd :
 set_option linter.uppercaseLean3 false in
 #align NonemptyFinLinOrd_dual_comp_forget_to_LinOrd nonemptyFinLinOrd_dual_comp_forget_to_linOrd
 
-/-- The forgetful functor `NonemptyFinLinOrd ⥤ FinPartOrd` and `order_dual` commute. -/
+/-- The forgetful functor `NonemptyFinLinOrd ⥤ FinPartOrd` and `OrderDual` commute. -/
 def nonemptyFinLinOrdDualCompForgetToFinPartOrd :
     NonemptyFinLinOrd.dual ⋙ forget₂ NonemptyFinLinOrd FinPartOrd ≅
       forget₂ NonemptyFinLinOrd FinPartOrd ⋙ FinPartOrd.dual

diff --git a/Mathlib/Order/Category/PartOrd.lean b/Mathlib/Order/Category/PartOrd.lean
@@ -103,7 +103,7 @@ theorem partOrd_dual_comp_forget_to_preord :
 set_option linter.uppercaseLean3 false in
 #align PartOrd_dual_comp_forget_to_Preord partOrd_dual_comp_forget_to_preord
 
-/-- `antisymmetrization` as a functor. It is the free functor. -/
+/-- `Antisymmetrization` as a functor. It is the free functor. -/
 def preordToPartOrd : Preord.{u} ⥤ PartOrd where
   obj X := PartOrd.of (Antisymmetrization X (· ≤ ·))
   map f := f.antisymmetrization
@@ -116,7 +116,7 @@ def preordToPartOrd : Preord.{u} ⥤ PartOrd where
 set_option linter.uppercaseLean3 false in
 #align Preord_to_PartOrd preordToPartOrd
 
-/-- `Preord_to_PartOrd` is left adjoint to the forgetful functor, meaning it is the free
+/-- `preordToPartOrd` is left adjoint to the forgetful functor, meaning it is the free
 functor from `Preord` to `PartOrd`. -/
 def preordToPartOrdForgetAdjunction :
     preordToPartOrd.{u} ⊣ forget₂ PartOrd Preord :=