Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-23 13:50 62acd6b8

View on Github →

chore(CommRing/adjunctions): refactor proofs (#1049)

  • splitting adjunction.lean
  • chore(CommRing/adjunctions): refactor proofs
  • remove unnecessary assumptions
  • add helpful doc-string
  • cleanup
  • breaking things, haven't finished yet
  • deterministic timeout
  • unfold_coes to the rescue
  • one more int.cast
  • yet another int.cast
  • Update src/data/mv_polynomial.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • Update src/data/mv_polynomial.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • WIP
  • Fix build
  • Fix build

Estimated changes

modified theorem category_theory.types_comp
modified theorem category_theory.types_id
added theorem int.eq_cast'
added theorem mv_polynomial.hom_C
modified theorem mv_polynomial.rename_id
modified theorem mv_polynomial.rename_rename