2025-01-28 22:24
Mathlib/CategoryTheory/ChosenFiniteProducts/InfSemilattice.lean
feat (CategoryTheory): constructing chosen finite products for the preorder category of a meet-semilattice with a top element (#21094) …
Added CategoryTheory.SemilatticeInf.tensorUnit