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 theorem CommRing.comp_val
added def CommRing.forget
added theorem CommRing.id_val
added def CommRing.of
added def CommRing.to_Ring
added def CommRing
added def Ring.forget
added def Ring.of
added def Ring
added def CommRing.limit
added def CommMon.forget
added def CommMon.of
added def CommMon
added def Mon.forget
added def Mon.of
added def Mon
added inductive Mon.colimits.prequotient
added theorem Mon.colimits.quot_mul
added theorem Mon.colimits.quot_one
added inductive Mon.colimits.relation
added def AddCommGroup.of
added def AddCommGroup
added def Group.of
added def Group
added def Borel
added def Meas.of
added def Meas
added def Top.adj₁
added def Top.adj₂
added def Top.discrete
added def Top.forget
added def Top.of
added def Top.trivial
added def Top
added theorem Top.epi_iff_surjective
added theorem Top.mono_iff_injective
added def Top.colimit
added def Top.limit
added def Top.presheaf
added def TopCommRing.of
added structure TopCommRing