File tree Expand file tree Collapse file tree 3 files changed +4
-4
lines changed
CategoryTheory/Monoidal/Cartesian Expand file tree Collapse file tree 3 files changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -170,7 +170,7 @@ theorem absorbent_iff_eventually_nhdsNE_zero :
170170@ [deprecated (since := "2025-03-03" )]
171171alias absorbent_iff_eventually_nhdsWithin_zero := absorbent_iff_eventually_nhdsNE_zero
172172
173- alias ⟨Absorbent.eventually_nhdsNE_zero, _⟩ := absorbent_iff_eventually_nhdsWithin_zero
173+ alias ⟨Absorbent.eventually_nhdsNE_zero, _⟩ := absorbent_iff_eventually_nhdsNE_zero
174174
175175@ [deprecated (since := "2025-03-03" )]
176176alias Absorbent.eventually_nhdsWithin_zero := Absorbent.eventually_nhdsNE_zero
Original file line number Diff line number Diff line change @@ -123,7 +123,7 @@ def MonObj.ofRepresentableBy (F : Cᵒᵖ ⥤ MonCat.{w}) (α : (F ⋙ forget _)
123123@ [deprecated (since := "2025-03-07" )]
124124alias MonObjOfRepresentableBy := MonObj.ofRepresentableBy
125125
126- @ [deprecated (since := "2025-09-09" )] alias Mon_ClassOfRepresentableBy := MonObjOfRepresentableBy
126+ @ [deprecated (since := "2025-09-09" )] alias Mon_ClassOfRepresentableBy := MonObj.ofRepresentableBy
127127
128128/-- If `M` is a monoid object, then `Hom(X, M)` has a monoid structure. -/
129129abbrev Hom.monoid : Monoid (X ⟶ M) where
@@ -268,7 +268,7 @@ alias MonObjOfRepresentableBy_yonedaMonObjRepresentableBy :=
268268
269269@ [deprecated (since := "2025-09-09" )]
270270alias Mon_ClassOfRepresentableBy_yonedaMonObjRepresentableBy :=
271- MonObjOfRepresentableBy_yonedaMonObjRepresentableBy
271+ MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy
272272
273273/-- The yoneda embedding for `Mon_C` is fully faithful. -/
274274def yonedaMonFullyFaithful : yonedaMon (C := C).FullyFaithful where
Original file line number Diff line number Diff line change @@ -177,7 +177,7 @@ theorem Pairwise.insert_of_symmetric_of_notMem (hs : s.Pairwise r) (hr : Symmetr
177177 (pairwise_insert_of_symmetric_of_notMem hr ha).2 ⟨hs, h⟩
178178
179179@ [deprecated (since := "2025-05-23" )]
180- alias Pairwise.insert_of_symmetric_of_not_mem := Pairwise.insert_of_symmetric_of_notMem
180+ alias Pairwise.insert_of_symmetric_of_not_mem := Pairwise.insert_of_symmetric
181181
182182theorem pairwise_pair : Set.Pairwise {a, b} r ↔ a ≠ b → r a b ∧ r b a := by simp [pairwise_insert]
183183
You can’t perform that action at this time.
0 commit comments