recreated the problem
03df6e2c
Proved that continuous functions are an algebra
80b9cab9
Merge branch 'master' into continuous_functions_algebra
d8ad078b
Solving a conflict appeared in sheaves
56d27165
Corrected a mistake in the documentation
da64672d
Solved a DANGEROUS INSTANCE problem
53b8e044
Forgot to remove #lint
fee8ca85
Making lint happy
dc6197b6
Trying again to make lint happy
b807d94a
Algebra structure over continuous bundled functions
4652e8a4
Trying to merge
20866d76
Having problems with the merging
99cee949
Updated the code following smooth manifolds PR
ac6c3bab
Merge branch 'master' into Lie_groups
c8f1304c
Merge branch 'master' into continuous_functions_algebra
f31adad3
Merge branch 'continuous_functions_algebra' into continuous_bundled_map
fd3efc70
Added some documentation
a9bdde6e
Merge branch 'Lie_groups' into smooth_map
1c3e998a
Begun writing smooth_functions
f91678ef
Merge branch 'master' into Lie_groups
46af74b2
Added some documentation
f5abebf3
Trying to show to Wojtek the excessive memory consumption
5288ed08
Merge branch 'master' into continuous_functions_algebra
3f5fa6d5
Forgot to save files before last commit.
ee83faa9
Merge branch 'master' into continuous_functions_algebra
37a21d49
Merge branch 'continuous_functions_algebra' into has_continuous_mul
629ad006
Merge branch 'has_continuous_mul' into continuous_bundled_map
ee812a2d
Added some further documentation
283dd6eb
Merge branch 'continuous_bundled_map' into smooth_map
3a3011dd
Merge branch 'continuous_bundled_map' into Lie_groups
fcb47140
Fixed dangerous instance
8e358bc7
Began implementing the smooth name
a8ef6259
halfway through the work on smooth maps
2bfd38dc
Begun generalizing constructions
81c590d5
Merge branch 'master' into Lie_groups
4fd7e93d
Ready to PR with help-needed
d99d42e3
Merge branch 'master' into Lie_groups
2e49c6ea
Adjust a mistake in last merge
9bbf9b36
complete times_cont_mdiff_within_at.prod_map
4ebee58c
Merge branch 'Lie_groups' into smooth_map
4c62301a
Merge branch 'master' into smooth_map
0dda2b57
smoothness of projections
0cedba63
proof terms
10142d08
Some progress on smooth maps
a1319a52
Applied most of suggested changes
ddd0b02c
Linter
0a73ef28
minor changes
485debfe
For Patrick: real numbers are a Lie group
726ed6c2
Merge branch 'master' into Lie_groups
1503909e
Changed folder name
b17d3d55
fix build
6a7aeba3
Merge remote-tracking branch 'upstream/master' into Lie_groups
34fd3b99
Merge branch 'Lie_groups' into smooth_map
0c15a403
Random commit
2a9c58b4
minor changes
92fe9150
streamline some proofs
652e523f
Update src/geometry/algebra/lie_group.lean
9c32b002
Update src/geometry/algebra/lie_group.lean
d6eb4fff
Random commit
f2e1b61f
Merge branch 'Lie_groups' of https://github.com/leanprover-community/…
41d41491
Applied most of suggested changes
3ceb3e90
Applied suggested changes
82f3a0d0
linter
2a1abc6b
Merge branch 'Lie_groups' into smooth_map
475c401e
Proved smooth functions valued in smooth algebra are algebra
5c95d717
Finished proofs of the PR
4cf09b77
Merge branch 'master' into smooth_map
8ea7f169
Reorganized files
0d68a6d6
Trying to fix the errors of the merge
4466d901
Fixed some errors
964085ad
Most of Linter
f2b74bd4
Solved dangerous instance problem
4fe39f07
Improved notation
e9f9fcb9
Random commit
e0c4b0d6
Finished stub on derivations
7c5b0ee9
Applied some of the suggested changes
770974ce
Some linter
da044086
More linter
0185535c
Done some progress
28ee5e94
Applied most of suggested changes
4ff259b2
Merge branch 'master' into smooth_map
7a7b852e
Partial progress
31ebd602
Merge branch 'derivations' into Lie_group_algebra
27ca5c07
Changing names
bab1a6a3
Random commit
5e789d0e
Random commit
4b2251e0
Merge branch 'derivations' into Lie_group_algebra
14eb0a50
Random commit
842b9a6c
Going back
b5147619
Random commit
9a349d2e
Merge branch 'master' into smooth_map
1ccee563
Random_commit
0f989f69
Let's PR the easy stuff first
ef30bdb7
Merge branch 'smooth_map' into Lie_group_algebra
4ae3499b
Solved most of the problems
2813ca65
Random commit
bf8b04f6
Merge branch 'master' into derivations
16c9fca3
Random commit
aa7241dd
Applied all suggested changes
94e62356
Linter
5dc59fa9
Applied Oliver's suggestions.
70a9590a
Updated documentation
f07e1f6f
Random commit
e66d2805
Applied most suggestions from code review
59681df8
Applied other suggested changes
ab8e448a
Merge branch 'master' into derivations
d6449fc1
Solving post-merge problems
fbadde28
Merge branch 'derivations' into Lie_group_algebra
bc77ae54
Minor change
e402c25d
Began to generalize to C^n
d3bea89e
Merge branch 'smooth_map' into diffeomorph
2ad5f2c2
First stab at diffeomorph
c1b1247c
Merge branch 'Lie_group_algebra' into smooth_bundle
2df47f66
Random commit
ac9dbeae
Merge branch 'master' into smooth_map
2e9a5157
Some better idea for generalization
8da70972
Merge branch 'smooth_map' into diffeomorph
03b9b058
Merge branch 'diffeomorph' into smooth_bundle
2d7f09e2
Finished the basic skeleton
64f06864
First stab at curves
12a6541a
Merge branch 'master' into curves
74553bc7
Post-merge fixes
e107d2b2
Lint
547a9e47
Nicknamen
changed the title
Nicknamen
commented
on 2021-06-27
Login to write a write a comment.
Login via GitHub