chore: classify new definition porting notes (#11512)

Classifies by adding issue number #11446 to porting notes claiming "added definition".
leanprover-community · Mar 26, 2024 · 79fb032 · 79fb032
1 parent aa68106
commit 79fb032
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Lie/UniversalEnveloping.lean b/Mathlib/Algebra/Lie/UniversalEnveloping.lean
@@ -88,7 +88,7 @@ def mkAlgHom : TensorAlgebra R L →ₐ[R] UniversalEnvelopingAlgebra R L :=
 variable {L}
 
 /-- The natural Lie algebra morphism from a Lie algebra to its universal enveloping algebra. -/
-@[simps!] -- Porting note: added
+@[simps!] -- Porting note (#11445): added
 def ι : L →ₗ⁅R⁆ UniversalEnvelopingAlgebra R L :=
   { (mkAlgHom R L).toLinearMap.comp ιₜ with
     map_lie' := fun {x y} => by

diff --git a/Mathlib/CategoryTheory/Sites/Grothendieck.lean b/Mathlib/CategoryTheory/Sites/Grothendieck.lean
@@ -424,7 +424,7 @@ instance : Coe (J.Cover X) (Sieve X) :=
 -/
 
 /-
-Porting note: Added this def as a replacement for the "dangerous" `Coe` above.
+Porting note (#11445): Added this def as a replacement for the "dangerous" `Coe` above.
 -/
 /-- The sieve associated to a term of `J.Cover X`.-/
 def sieve (S : J.Cover X) : Sieve X := S.1

diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean
@@ -837,7 +837,7 @@ end IsMultiplicative
 section SpecialFunctions
 
 /-- The identity on `ℕ` as an `ArithmeticFunction`.  -/
-nonrec  -- Porting note: added
+nonrec  -- Porting note (#11445): added
 def id : ArithmeticFunction ℕ :=
   ⟨id, rfl⟩
 #align nat.arithmetic_function.id ArithmeticFunction.id

diff --git a/Mathlib/SetTheory/Game/Basic.lean b/Mathlib/SetTheory/Game/Basic.lean
@@ -49,7 +49,7 @@ abbrev Game :=
 
 namespace Game
 
--- Porting note: added this definition
+-- Porting note (#11445): added this definition
 /-- Negation of games. -/
 instance : Neg Game where
   neg := Quot.map Neg.neg <| fun _ _ => (neg_equiv_neg_iff).2