mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(CategoryTheory): more lemmas for the calculus of fractions

Open joelriou opened this issue 1 year ago • 1 comments

We introduce lemmas on fractions which shall be useful when construction the preadditive structure on the localized category.

  • [ ] depends on: #11721

Open in Gitpod

joelriou avatar Mar 28 '24 09:03 joelriou

This PR/issue depends on:

  • ~~leanprover-community/mathlib4#11721~~ By Dependent Issues (🤖). Happy coding!

leanprover-community-mathlib4-bot avatar Mar 29 '24 11:03 leanprover-community-mathlib4-bot

bors merge

kim-em avatar Apr 18 '24 01:04 kim-em

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar Apr 18 '24 01:04 mathlib-bors[bot]