Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 9a0f643

Browse files
pitmonticonericcardobrasca
authored andcommittedMar 1, 2024
chore: classify added lemma porting notes (#10885)
Classifies by adding number (#10756) to porting notes claiming `added lemma`.
1 parent fc348a8 commit 9a0f643

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed
 

‎Mathlib/Algebra/Homology/HomotopyCategory.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -249,7 +249,7 @@ def Functor.mapHomotopyCategory (F : V ⥤ W) [F.Additive] (c : ComplexShape ι)
249249
(fun _ _ _ _ ⟨h⟩ => HomotopyCategory.eq_of_homotopy _ _ (F.mapHomotopy h))
250250
#align category_theory.functor.map_homotopy_category CategoryTheory.Functor.mapHomotopyCategory
251251

252-
-- porting note: added this lemma because of the new definition of `Functor.mapHomotopyCategory`
252+
-- Porting note (#10756): added lemma because of new definition of `Functor.mapHomotopyCategory`
253253
@[simp]
254254
lemma Functor.mapHomotopyCategory_map (F : V ⥤ W) [F.Additive] {c : ComplexShape ι}
255255
{K L : HomologicalComplex V c} (f : K ⟶ L) :

‎Mathlib/RingTheory/FractionalIdeal/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -208,7 +208,7 @@ theorem coe_mk (I : Submodule R P) (hI : IsFractional S I) :
208208
rfl
209209
#align fractional_ideal.coe_mk FractionalIdeal.coe_mk
210210

211-
-- Porting note: added this lemma because Lean can't see through the composition of coercions.
211+
-- Porting note (#10756): added lemma because Lean can't see through the composition of coercions.
212212
theorem coeToSet_coeToSubmodule (I : FractionalIdeal S P) :
213213
((I : Submodule R P) : Set P) = I :=
214214
rfl

0 commit comments

Comments
 (0)
Please sign in to comment.