Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-31 06:43 2db435d8

View on Github →

chore(category_theory): move all instances (e.g. Top, CommRing, Meas) into the root namespace (#1074)

  • splitting adjunction.lean
  • chore(CommRing/adjunctions): refactor proofs
  • remove unnecessary assumptions
  • add helpful doc-string
  • cleanup
  • chore(category_theory): move all instances (e.g. Top, CommRing, Meas) to the root namespace
  • minor
  • breaking things, haven't finished yet
  • deterministic timeout
  • unfold_coes to the rescue
  • one more int.cast
  • yet another int.cast
  • fix merge
  • minor
  • merge
  • fix imports
  • fix merge
  • fix imports/namespaces
  • more namespace fixes
  • fixes
  • delete stray file

Estimated changes

added inductive Mon.colimits.prequotient
added theorem Mon.colimits.quot_mul
added theorem Mon.colimits.quot_one
added inductive Mon.colimits.relation