chore: classify added lemma porting notes (#10885)

Classifies by adding number (#10756) to porting notes claiming `added lemma`.
leanprover-community · Feb 23, 2024 · 1bd0ec5 · 1bd0ec5
1 parent 98d430d
commit 1bd0ec5
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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