mathlib3
feat(geometry/manifold/curves): smooth curves
#8103
Open

Commits
  • recreated the problem
    Nicknamen committed 6 years ago
  • Proved that continuous functions are an algebra
    Nicknamen committed 6 years ago
  • Merge branch 'master' into continuous_functions_algebra
    Nicknamen committed 6 years ago
  • Solving a conflict appeared in sheaves
    Nicknamen committed 6 years ago
  • Corrected a mistake in the documentation
    Nicknamen committed 6 years ago
  • Solved a DANGEROUS INSTANCE problem
    Nicknamen committed 6 years ago
  • Forgot to remove #lint
    Nicknamen committed 6 years ago
  • Making lint happy
    Nicknamen committed 6 years ago
  • Trying again to make lint happy
    Nicknamen committed 6 years ago
  • Algebra structure over continuous bundled functions
    Nicknamen committed 6 years ago
  • Trying to merge
    Nicknamen committed 6 years ago
  • Having problems with the merging
    Nicknamen committed 6 years ago
  • Updated the code following smooth manifolds PR
    Nicknamen committed 6 years ago
  • Merge branch 'master' into Lie_groups
    Nicknamen committed 6 years ago
  • Merge branch 'master' into continuous_functions_algebra
    Nicknamen committed 6 years ago
  • Merge branch 'continuous_functions_algebra' into continuous_bundled_map
    Nicknamen committed 6 years ago
  • Added some documentation
    Nicknamen committed 6 years ago
  • Merge branch 'Lie_groups' into smooth_map
    Nicknamen committed 6 years ago
  • Begun writing smooth_functions
    Nicknamen committed 6 years ago
  • Merge branch 'master' into Lie_groups
    Nicknamen committed 6 years ago
  • Added some documentation
    Nicknamen committed 6 years ago
  • Trying to show to Wojtek the excessive memory consumption
    Nicknamen committed 6 years ago
  • Merge branch 'master' into continuous_functions_algebra
    Nicknamen committed 6 years ago
  • Forgot to save files before last commit.
    Nicknamen committed 6 years ago
  • Merge branch 'master' into continuous_functions_algebra
    Nicknamen committed 6 years ago
  • Merge branch 'continuous_functions_algebra' into has_continuous_mul
    Nicknamen committed 6 years ago
  • Merge branch 'has_continuous_mul' into continuous_bundled_map
    Nicknamen committed 6 years ago
  • Added some further documentation
    Nicknamen committed 6 years ago
  • Merge branch 'continuous_bundled_map' into smooth_map
    Nicknamen committed 6 years ago
  • Merge branch 'continuous_bundled_map' into Lie_groups
    Nicknamen committed 6 years ago
  • Fixed dangerous instance
    Nicknamen committed 6 years ago
  • Began implementing the smooth name
    Nicknamen committed 6 years ago
  • halfway through the work on smooth maps
    Nicknamen committed 6 years ago
  • Begun generalizing constructions
    Nicknamen committed 6 years ago
  • Merge branch 'master' into Lie_groups
    Nicknamen committed 6 years ago
  • Ready to PR with help-needed
    Nicknamen committed 6 years ago
  • Merge branch 'master' into Lie_groups
    Nicknamen committed 6 years ago
  • Adjust a mistake in last merge
    Nicknamen committed 6 years ago
  • complete times_cont_mdiff_within_at.prod_map
    sgouezel committed 6 years ago
  • Merge branch 'Lie_groups' into smooth_map
    Nicknamen committed 6 years ago
  • Merge branch 'master' into smooth_map
    Nicknamen committed 6 years ago
  • smoothness of projections
    sgouezel committed 6 years ago
  • proof terms
    sgouezel committed 6 years ago
  • Some progress on smooth maps
    Nicknamen committed 6 years ago
  • Applied most of suggested changes
    Nicknamen committed 6 years ago
  • Linter
    Nicknamen committed 6 years ago
  • minor changes
    Nicknamen committed 6 years ago
  • For Patrick: real numbers are a Lie group
    Nicknamen committed 6 years ago
  • Merge branch 'master' into Lie_groups
    Nicknamen committed 6 years ago
  • Changed folder name
    Nicknamen committed 6 years ago
  • fix build
    sgouezel committed 6 years ago
  • Merge remote-tracking branch 'upstream/master' into Lie_groups
    sgouezel committed 6 years ago
  • Merge branch 'Lie_groups' into smooth_map
    Nicknamen committed 6 years ago
  • Random commit
    Nicknamen committed 6 years ago
  • minor changes
    Nicknamen committed 6 years ago
  • streamline some proofs
    sgouezel committed 6 years ago
  • Update src/geometry/algebra/lie_group.lean
    Nicknamen committed 6 years ago
  • Update src/geometry/algebra/lie_group.lean
    Nicknamen committed 6 years ago
  • Random commit
    Nicknamen committed 6 years ago
  • Merge branch 'Lie_groups' of https://github.com/leanprover-community/mathlib into Lie_groups
    Nicknamen committed 6 years ago
  • Applied most of suggested changes
    Nicknamen committed 6 years ago
  • Applied suggested changes
    Nicknamen committed 6 years ago
  • linter
    Nicknamen committed 6 years ago
  • Merge branch 'Lie_groups' into smooth_map
    Nicknamen committed 6 years ago
  • Proved smooth functions valued in smooth algebra are algebra
    Nicknamen committed 6 years ago
  • Finished proofs of the PR
    Nicknamen committed 6 years ago
  • Merge branch 'master' into smooth_map
    Nicknamen committed 6 years ago
  • Reorganized files
    Nicknamen committed 6 years ago
  • Trying to fix the errors of the merge
    Nicknamen committed 6 years ago
  • Fixed some errors
    Nicknamen committed 6 years ago
  • Most of Linter
    Nicknamen committed 6 years ago
  • Solved dangerous instance problem
    Nicknamen committed 6 years ago
  • Improved notation
    Nicknamen committed 6 years ago
  • Random commit
    Nicknamen committed 6 years ago
  • Finished stub on derivations
    Nicknamen committed 6 years ago
  • Applied some of the suggested changes
    Nicknamen committed 6 years ago
  • Some linter
    Nicknamen committed 6 years ago
  • More linter
    Nicknamen committed 6 years ago
  • Done some progress
    Nicknamen committed 6 years ago
  • Applied most of suggested changes
    Nicknamen committed 6 years ago
  • Merge branch 'master' into smooth_map
    Nicknamen committed 6 years ago
  • Partial progress
    Nicknamen committed 6 years ago
  • Merge branch 'derivations' into Lie_group_algebra
    Nicknamen committed 6 years ago
  • Changing names
    Nicknamen committed 6 years ago
  • Random commit
    Nicknamen committed 6 years ago
  • Random commit
    Nicknamen committed 6 years ago
  • Merge branch 'derivations' into Lie_group_algebra
    Nicknamen committed 6 years ago
  • Random commit
    Nicknamen committed 6 years ago
  • Going back
    Nicknamen committed 6 years ago
  • Random commit
    Nicknamen committed 6 years ago
  • Merge branch 'master' into smooth_map
    Nicknamen committed 6 years ago
  • Random_commit
    Nicknamen committed 6 years ago
  • Let's PR the easy stuff first
    Nicknamen committed 6 years ago
  • Merge branch 'smooth_map' into Lie_group_algebra
    Nicknamen committed 6 years ago
  • Solved most of the problems
    Nicknamen committed 6 years ago
  • Random commit
    Nicknamen committed 6 years ago
  • Merge branch 'master' into derivations
    Nicknamen committed 6 years ago
  • Random commit
    Nicknamen committed 6 years ago
  • Applied all suggested changes
    Nicknamen committed 6 years ago
  • Linter
    Nicknamen committed 6 years ago
  • + more commits ...
Loading