Commit 2023-05-02 10:23 2bdc8a9e

View on Github →

feat: port CategoryTheory.Monoidal.Tor (#3754)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Tor.lean

added def CategoryTheory.Tor'

added theorem CategoryTheory.Tor'_map_app'

added theorem CategoryTheory.Tor'_obj_map

added def CategoryTheory.Tor

added def CategoryTheory.tor'SuccOfProjective

added def CategoryTheory.torSuccOfProjective