File tree Expand file tree Collapse file tree
Mathlib/CategoryTheory/Limits/Constructions Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -89,7 +89,7 @@ variable [HasBinaryProducts C] [HasTerminal C]
8989
9090/-- If `C` has a terminal object and binary products, then it has a product for objects indexed by
9191`Fin n`.
92- This is a helper lemma for `hasFiniteProductsOfHasBinaryAndTerminal `, which is more general
92+ This is a helper lemma for `hasFiniteProducts_of_has_binary_and_terminal `, which is more general
9393than this.
9494-/
9595private theorem hasProduct_fin : ∀ (n : ℕ) (f : Fin n → C), HasProduct f
@@ -213,7 +213,7 @@ variable [HasBinaryCoproducts C] [HasInitial C]
213213/--
214214If `C` has an initial object and binary coproducts, then it has a coproduct for objects indexed by
215215`Fin n`.
216- This is a helper lemma for `hasCofiniteProductsOfHasBinaryAndTerminal `, which is more general
216+ This is a helper lemma for `hasFiniteCoproducts_of_has_binary_and_initial `, which is more general
217217than this.
218218-/
219219private theorem hasCoproduct_fin : ∀ (n : ℕ) (f : Fin n → C), HasCoproduct f
You can’t perform that action at this time.
0 commit comments