mathlib3
refactor(topology/continuous_function/bounded): make arithmetic computable
#12075
Open
Overview
Commits
25
Changes
View On GitHub
Commits
  • feat(topology/continuous_function/algebra): generalize algebra instances
    eric-wieser committed 4 years ago
  • Update basic.lean
    eric-wieser committed 4 years ago
  • Update limits.lean
    eric-wieser committed 4 years ago
  • fix
    eric-wieser committed 4 years ago
  • fix name clash
    eric-wieser committed 4 years ago
  • fix
    eric-wieser committed 4 years ago
  • fix rename
    eric-wieser committed 4 years ago
  • add rfl lemmas, simplify proof
    eric-wieser committed 4 years ago
  • oops
    eric-wieser committed 4 years ago
  • fix
    eric-wieser committed 4 years ago
  • fix rename
    eric-wieser committed 4 years ago
  • fix
    eric-wieser committed 4 years ago
  • chore(topology/continuous_function/bounded): make the algebraic structure computable
    eric-wieser committed 4 years ago
  • refactor(topology/continuous_function/bounded): make arithmetic computable
    eric-wieser committed 4 years ago
  • whoops
    eric-wieser committed 4 years ago
  • fix
    eric-wieser committed 4 years ago
  • Merge branch 'master' into eric-wieser/bounded-computable
    eric-wieser committed 4 years ago
  • Merge branch 'master' into eric-wieser/bounded-computable
    eric-wieser committed 4 years ago
  • fix
    eric-wieser committed 4 years ago
  • Merge branch 'master' into eric-wieser/bounded-computable
    eric-wieser committed 4 years ago
  • fix tests
    eric-wieser committed 4 years ago
  • Merge branch 'master' into eric-wieser/bounded-computable
    eric-wieser committed 4 years ago
  • fix merge conflicts
    eric-wieser committed 4 years ago
  • Merge remote-tracking branch 'origin/master' into eric-wieser/bounded-computable
    eric-wieser committed 3 years ago
  • cut back changes:
    eric-wieser committed 3 years ago
FAQ Terms Privacy Refunds Impressum
Loading