chore: classify added lemma porting notes (#10757)

Classifies by adding issue number (#10756) to porting notes claiming `added lemma`.
leanprover-community · Feb 20, 2024 · a5e4848 · a5e4848
1 parent ecce7d9
commit a5e4848
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git a/Mathlib/Algebra/Category/GroupWithZeroCat.lean b/Mathlib/Algebra/Category/GroupWithZeroCat.lean
@@ -60,10 +60,10 @@ instance {M N : GroupWithZeroCat} : FunLike (M ⟶ N) M N :=
     apply DFunLike.coe_injective'
     exact h⟩
 
--- porting note: added
+-- Porting note (#10756): added lemma
 lemma coe_id {X : GroupWithZeroCat} : (𝟙 X : X → X) = id := rfl
 
--- porting note: added
+-- Porting note (#10756): added lemma
 lemma coe_comp {X Y Z : GroupWithZeroCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
 instance groupWithZeroConcreteCategory : ConcreteCategory GroupWithZeroCat where

diff --git a/Mathlib/Algebra/Category/Ring/Basic.lean b/Mathlib/Algebra/Category/Ring/Basic.lean
@@ -85,10 +85,10 @@ instance instFunLike {X Y : SemiRingCat} : FunLike (X ⟶ Y) X Y :=
 instance instRingHomClass {X Y : SemiRingCat} : RingHomClass (X ⟶ Y) X Y :=
   RingHom.instRingHomClass
 
--- porting note: added
+-- Porting note (#10756): added lemma
 lemma coe_id {X : SemiRingCat} : (𝟙 X : X → X) = id := rfl
 
--- porting note: added
+-- Porting note (#10756): added lemma
 lemma coe_comp {X Y Z : SemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
 -- porting note: added
@@ -209,10 +209,10 @@ instance instFunLike {X Y : RingCat} : FunLike (X ⟶ Y) X Y :=
 instance instRingHomClass {X Y : RingCat} : RingHomClass (X ⟶ Y) X Y :=
   RingHom.instRingHomClass
 
--- porting note: added
+-- Porting note (#10756): added lemma
 lemma coe_id {X : RingCat} : (𝟙 X : X → X) = id := rfl
 
--- porting note: added
+-- Porting note (#10756): added lemma
 lemma coe_comp {X Y Z : RingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
 -- porting note: added
@@ -315,10 +315,10 @@ instance instFunLike {X Y : CommSemiRingCat} : FunLike (X ⟶ Y) X Y :=
 instance instRingHomClass {X Y : CommSemiRingCat} : RingHomClass (X ⟶ Y) X Y :=
   RingHom.instRingHomClass
 
--- porting note: added
+-- Porting note (#10756): added lemma
 lemma coe_id {X : CommSemiRingCat} : (𝟙 X : X → X) = id := rfl
 
--- porting note: added
+-- Porting note (#10756): added lemma
 lemma coe_comp {X Y Z : CommSemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
 -- porting note: added
@@ -435,10 +435,10 @@ instance instFunLike {X Y : CommRingCat} : FunLike (X ⟶ Y) X Y :=
 instance instRingHomClass {X Y : CommRingCat} : RingHomClass (X ⟶ Y) X Y :=
   RingHom.instRingHomClass
 
--- porting note: added
+-- Porting note (#10756): added lemma
 lemma coe_id {X : CommRingCat} : (𝟙 X : X → X) = id := rfl
 
--- porting note: added
+-- Porting note (#10756): added lemma
 lemma coe_comp {X Y Z : CommRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
 -- porting note: added