Commit 2019-06-16 19:28 7b715eb6

View on Github →

Direct limit of modules, abelian groups, rings, and fields. (#754)

  • stuff
  • stuff
  • more stuff
  • pre merge commit
  • prove of_zero.exact
  • remove silly rewrite
  • slightly shorten proof
  • direct limit of modules
  • upgrade mathlib
  • direct limit of rings
  • direct limit of fields (WIP)
  • trying to prove zero_exact for rings
  • use sqrt 2 instead of F4
  • direct limit of field
  • cleanup for mathlib
  • remove ununsed lemmas
  • clean up
  • docstrings
  • local
  • fix build
  • Replace real with polynomial int in proof
  • Update basic.lean

Estimated changes

added theorem ring.direct_limit.of_f