mathlib3
refactor(topology/continuous_function/bounded): make arithmetic computable
#12075
Open
Open
refactor(topology/continuous_function/bounded): make arithmetic computable #12075
eric-wieser
wants to merge
25 commits into
master
from
eric-wieser/bounded-computable
feat(topology/continuous_function/algebra): generalize algebra instances
8cac1dfb
Update basic.lean
7ddfbc01
Update limits.lean
3c3928ad
fix
629771f3
fix name clash
7b8639d7
fix
ced67bf9
fix rename
3c2d858e
add rfl lemmas, simplify proof
f5c6aeca
oops
3813ff30
fix
07d21314
fix rename
58d65d1d
fix
4df9d1e5
chore(topology/continuous_function/bounded): make the algebraic struc…
d347306b
refactor(topology/continuous_function/bounded): make arithmetic compu…
6788d42d
whoops
d79e0084
fix
99f3411f
Merge branch 'master' into eric-wieser/bounded-computable
9452cb9f
Merge branch 'master' into eric-wieser/bounded-computable
30d85247
fix
e7853729
Merge branch 'master' into eric-wieser/bounded-computable
b5fcbc91
fix tests
7ccca1f1
Merge branch 'master' into eric-wieser/bounded-computable
1d175c97
fix merge conflicts
c66cc7e0
Merge remote-tracking branch 'origin/master' into eric-wieser/bounded…
f00f94fe
cut back changes:
bf722019
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author
merge-conflict
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub