diff --git a/Mathlib/Algebra/Homology/HomotopyCategory.lean b/Mathlib/Algebra/Homology/HomotopyCategory.lean
index 4a0ee591995db..e69c5c0826f7a 100644
--- a/Mathlib/Algebra/Homology/HomotopyCategory.lean
+++ b/Mathlib/Algebra/Homology/HomotopyCategory.lean
@@ -249,7 +249,7 @@ def Functor.mapHomotopyCategory (F : V ⥤ W) [F.Additive] (c : ComplexShape ι)
     (fun _ _ _ _ ⟨h⟩ => HomotopyCategory.eq_of_homotopy _ _ (F.mapHomotopy h))
 #align category_theory.functor.map_homotopy_category CategoryTheory.Functor.mapHomotopyCategory
 
--- porting note: added this lemma because of the new definition of `Functor.mapHomotopyCategory`
+-- Porting note (#10756): added lemma because of new definition of `Functor.mapHomotopyCategory`
 @[simp]
 lemma Functor.mapHomotopyCategory_map (F : V ⥤ W) [F.Additive] {c : ComplexShape ι}
     {K L : HomologicalComplex V c} (f : K ⟶ L) :
diff --git a/Mathlib/RingTheory/FractionalIdeal/Basic.lean b/Mathlib/RingTheory/FractionalIdeal/Basic.lean
index 377ab6a4a7fad..2f602cb141b5a 100644
--- a/Mathlib/RingTheory/FractionalIdeal/Basic.lean
+++ b/Mathlib/RingTheory/FractionalIdeal/Basic.lean
@@ -208,7 +208,7 @@ theorem coe_mk (I : Submodule R P) (hI : IsFractional S I) :
   rfl
 #align fractional_ideal.coe_mk FractionalIdeal.coe_mk
 
--- Porting note: added this lemma because Lean can't see through the composition of coercions.
+-- Porting note (#10756): added lemma because Lean can't see through the composition of coercions.
 theorem coeToSet_coeToSubmodule (I : FractionalIdeal S P) :
     ((I : Submodule R P) : Set P) = I :=
   rfl