mathlib3
refactor(analysis/normed/group/basic): unbundle algebra from norm structure
#18462
Open
Open
refactor(analysis/normed/group/basic): unbundle algebra from norm structure #18462
eric-wieser
wants to merge
40 commits into
master
from
eric-wieser/unbundle-normed-algebra
refactor(analysis/normed/group/basic): unbundle algebra from norm str…
3d1dde9c
one more file
a466c033
fix
342bf4d1
normed_space fixes
f935866a
more
c98333f3
more
a6943083
automated replacements
7a743162
more
b9989324
more
9bed7232
eric-wieser
commented
on 2023-02-17
untested changes
a5cd4c92
more
ed568d93
Regex search for `(?<=Type\*[)}] )\[(semi_?)?normed_(add_comm_group […
f4bf66c1
rebuild cache
01848291
add a missing base class
a9566e78
two more fixes
42c4b667
more fixes
97c4c2b2
fix a broken proof
c9115217
extra underscore
30edb9d7
fix
822bf296
fixes
f35943af
fix
125852f8
fix
528fb3fb
fix
d037fc08
more
37fba2fc
help with elaboration order
0215721e
fix
ec1b2335
fix
f5213781
more easy fixes
b0376330
fix
f583fba8
underscores
51235b2f
more fixes
248f2c24
missing derive
9e8d199e
more additions
59b0bfd4
more additions
b5edbe1c
_
288f5826
more arguments
767231af
fix timeout
2ff5f99f
arguments
2bbecc2d
easy fixes in a doomed file
aec45cf2
_
452cead1
Reviewers
No reviews
Assignees
No one assigned
Labels
WIP
RFC
t-analysis
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub