Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: Integral curves are either injective or periodic #9343

Closed
wants to merge 225 commits into from
Closed

[Merged by Bors] - feat: Integral curves are either injective or periodic #9343

wants to merge 225 commits into from

Commits on Nov 13, 2023

  1. doc

    @winstonyin
    winstonyin committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    4e53e96 View commit details
    Browse the repository at this point in the history

Commits on Nov 17, 2023

  1. compiles

    @winstonyin
    winstonyin committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    f14b378 View commit details
    Browse the repository at this point in the history

  2. indent

    @winstonyin
    winstonyin committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    22b4f1f View commit details
    Browse the repository at this point in the history

  3. import, indent

    @winstonyin
    winstonyin committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    0747174 View commit details
    Browse the repository at this point in the history

  4. docstring

    @winstonyin
    winstonyin committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    23d691f View commit details
    Browse the repository at this point in the history

  5. Mathlib.lean

    @winstonyin
    winstonyin committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    e8e7338 View commit details
    Browse the repository at this point in the history

  6. lake manifest

    @winstonyin
    winstonyin committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    ccc8f77 View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'origin/master' into integral_curve

    @winstonyin
    winstonyin committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    42341d1 View commit details
    Browse the repository at this point in the history

Commits on Nov 18, 2023

  1. removed temporary notation

    @winstonyin
    winstonyin committed Nov 18, 2023
    Configuration menu
    Copy the full SHA
    720ec35 View commit details
    Browse the repository at this point in the history

  2. integralCurveAt, change PicardLindelof statement order

    @winstonyin
    winstonyin committed Nov 18, 2023
    Configuration menu
    Copy the full SHA
    25f1065 View commit details
    Browse the repository at this point in the history

  3. compiles

    @winstonyin
    winstonyin committed Nov 18, 2023
    Configuration menu
    Copy the full SHA
    d4139b6 View commit details
    Browse the repository at this point in the history

Commits on Nov 19, 2023

  1. Sketch a section on interior and boundary of manifolds.

    @grunweg
    grunweg committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    4b57dfe View commit details
    Browse the repository at this point in the history

  2. More progress. Tweaks, polish and fleshing out some sorries. 

    - use lowerCamelCase for our definitions, per the naming convention.
- sketch how to prove a few more sorries.
    @grunweg
    grunweg committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    e9d3546 View commit details
    Browse the repository at this point in the history

  3. One more lemma.

    @grunweg
    grunweg committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    cbd22f4 View commit details
    Browse the repository at this point in the history

  4. One lemma was in mathlib. :-)

    @grunweg
    grunweg committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    0dbf3b0 View commit details
    Browse the repository at this point in the history

  5. Fix the build; mild clean-ups.

    @grunweg
    grunweg committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    a978f02 View commit details
    Browse the repository at this point in the history

  6. Small simplifications.

    @grunweg
    grunweg committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    1f6dbaa View commit details
    Browse the repository at this point in the history

Commits on Nov 20, 2023

  1. has -> is, docstring, shift/stretch lemmas

    @winstonyin
    winstonyin committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    9c58652 View commit details
    Browse the repository at this point in the history

  2. detailed proof steps

    @winstonyin
    winstonyin committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    6b55cbc View commit details
    Browse the repository at this point in the history

  3. open Set

    @winstonyin
    winstonyin committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    0ada08e View commit details
    Browse the repository at this point in the history

  4. IsIntegralCurveAt in preamble

    @winstonyin
    winstonyin committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    063822d View commit details
    Browse the repository at this point in the history

  5. IsIntegralCurveAt.comp_add

    @winstonyin
    winstonyin committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    fb4196f View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2023

  1. translation, scale, and reverse lemmas

    @winstonyin
    winstonyin committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    6f665ad View commit details
    Browse the repository at this point in the history

  2. iff lemmas

    @winstonyin
    winstonyin committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    b59c82f View commit details
    Browse the repository at this point in the history

  3. Small polish. Note that smoothness is not required; 

    all results in this file hold for topological manifolds.
    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    3c2e424 View commit details
    Browse the repository at this point in the history

  4. The boundary is closed: entails showing that interior and boundary ar… 

    …e disjoint.
    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    c95243e View commit details
    Browse the repository at this point in the history

  5. Almost-proof that boundary has empty interior: need to adjust definit… 

    …ion.

The current lemma (frontier of (e.extend I).target) has contributions
from boundary(I.range) (good), but also from another factor (bad).
    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    933cc59 View commit details
    Browse the repository at this point in the history

  6. Correct the definition of boundary: 

    we should ask for x not being an interior of its chart's target.
(Asking for "lies in the frontier", as we did before, would also include
boundary points of (extChartAt I x).source in interior (range I),
which we're not interested in.)
In other words, the previous definition was actually *wrong*.
    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    2041d30 View commit details
    Browse the repository at this point in the history

  7. Fix and complete proof that the boundary has empty interior.

    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    f1fda32 View commit details
    Browse the repository at this point in the history

  8. Small clean-ups: 

    - make some variables explicit; fix namespacing of one result.
- move all topology helper results into their own section.
    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    6a4e39c View commit details
    Browse the repository at this point in the history

  9. Clean up lemmas about boundary.

    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    88bea4c View commit details
    Browse the repository at this point in the history

  10. Small golfs.

    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    73e203f View commit details
    Browse the repository at this point in the history

  11. Fix rebase, make it build and fix a docstring typo.

    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    90090b2 View commit details
    Browse the repository at this point in the history

  12. Fix casing for real: IsInteriorPoint is correct.

    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    338ab9f View commit details
    Browse the repository at this point in the history

  13. Name lemma in snake_case.

    @grunweg
    grunweg committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    378088c View commit details
    Browse the repository at this point in the history

Commits on Nov 22, 2023

  1. naming

    @winstonyin
    winstonyin committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    efe0880 View commit details
    Browse the repository at this point in the history

  2. move lemma, style

    @winstonyin
    winstonyin committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    d35e843 View commit details
    Browse the repository at this point in the history

  3. Define topological manifolds and use them for defining interior and b… 

    …oundary.

TODO: add to SmoothManifoldsWithCorners' docstring
- does mathlib have the implication smooth mfd => top mfd? (most is there for sure)
- do I want this, or should I just "contGroupoid H" and that suffices?
    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    dce81a6 View commit details
    Browse the repository at this point in the history

  4. Alternative, more minimal fix. 

    Then, implication is mostly handled by the type-class system. Hmm.
    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    79fcb13 View commit details
    Browse the repository at this point in the history

  5. sketch boundary argument

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    e1a9363 View commit details
    Browse the repository at this point in the history

  6. MAYBE this tweak makes the proof easier. 

    It shouldn't make it harder, though. One proof broken, not fixed yet. Should not be bad in principle.
    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    f38f823 View commit details
    Browse the repository at this point in the history

  7. Cleanup, one easy sorry.

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    07d1dbc View commit details
    Browse the repository at this point in the history

  8. Another easy sorry.

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    c331ee2 View commit details
    Browse the repository at this point in the history

  9. Move a helper upfront; eliminating another sorry.

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    191a5c1 View commit details
    Browse the repository at this point in the history

  10. Starting at scifi lemma: might be science *fiction* actually...

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    66b1943 View commit details
    Browse the repository at this point in the history

  11. Small golfs.

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    7840b91 View commit details
    Browse the repository at this point in the history

  12. Extract lemmas used in the proof so far.

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    61fd70e View commit details
    Browse the repository at this point in the history

  13. Fill sorry in description of boundary.

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    5869bd5 View commit details
    Browse the repository at this point in the history

  14. Extract one more useful lemma; tiny golf.

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    058bb70 View commit details
    Browse the repository at this point in the history

  15. Simplify: use chart source instead of extChart.source. 

    That's the normal form (and conceptually simpler); jumping between these
different forms means I need to rewrite more often. Most of the time,
I don't care which one I use.

Delete a helper lemma about this bad normal form: shouldn't use that.
    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    7e1542d View commit details
    Browse the repository at this point in the history

  16. Fill in one more helper sorry.

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    219f85c View commit details
    Browse the repository at this point in the history

  17. Move helpers to better namespace; show a MapsTo version; 

    mathlib has a related version, with a slightly different formula...
    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    b97611e View commit details
    Browse the repository at this point in the history

  18. Reduce interior independence statement to a local lemma. 

    Extracting all those tiny lemmas still feels slightly weird, but I guess
they are still useful, somewhen. apply? cannot find them, at least.
    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    ef4c232 View commit details
    Browse the repository at this point in the history

  19. Give up: remove WIP claim that boundary as empty interior. 

    I don't see how to show this, given the current hypotheses.
    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    184a062 View commit details
    Browse the repository at this point in the history

  20. Rename and golf mapsTo results for extended local homeos.

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    c634f1a View commit details
    Browse the repository at this point in the history

  21. Small golfs and clean-ups.

    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    dd9e73f View commit details
    Browse the repository at this point in the history

  22. Move complete (and now unused) helper results to their files: 

    I decided two MapsTo helpers are obvious enough to be left out,
but disjointness of interior and frontier is interesting enough.
    @grunweg
    grunweg committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    3d820be View commit details
    Browse the repository at this point in the history

  23. compiles

    @winstonyin
    winstonyin committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    2c69553 View commit details
    Browse the repository at this point in the history

Commits on Nov 23, 2023

  1. new lemmas and slight golfing

    @winstonyin
    winstonyin committed Nov 23, 2023
    Configuration menu
    Copy the full SHA
    7c6bccf View commit details
    Browse the repository at this point in the history

Commits on Nov 25, 2023

  1. Essentials are complete.

    @grunweg
    grunweg committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    e74b860 View commit details
    Browse the repository at this point in the history

  2. Clean up; document TODOs/next steps; move all helpers to their proper… 

    … place.
    @grunweg
    grunweg committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    f8e3340 View commit details
    Browse the repository at this point in the history

  3. Remove helper lemmas not needed here.

    @grunweg
    grunweg committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    4febc74 View commit details
    Browse the repository at this point in the history

  4. Pare down interior/boundary file to the necesssary basics; sorry-free. 

    Everything else requires advanced technology not in mathlib yet.
    @grunweg
    grunweg committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    c1f3395 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'MR-manifolds-boundary' into integral_curve

    @grunweg
    grunweg committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    25ff469 View commit details
    Browse the repository at this point in the history

  6. Simplify.

    @grunweg
    grunweg committed Nov 25, 2023
    Configuration menu
    Copy the full SHA
    1459dfb View commit details
    Browse the repository at this point in the history

Commits on Nov 26, 2023

  1. compiles

    @winstonyin
    winstonyin committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    094ca88 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'integral_curve' of https://github.com/leanprover-commun… 

    …ity/mathlib4 into integral_curve
    @winstonyin
    winstonyin committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    ca11211 View commit details
    Browse the repository at this point in the history

  3. range_mem_nhds_isInteriorPoint

    @winstonyin
    winstonyin committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    7754760 View commit details
    Browse the repository at this point in the history

  4. namespace

    @winstonyin
    winstonyin committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    6033099 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/MR-manifolds-boundary' into inte… 

    …gral_curve
    @winstonyin
    winstonyin committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    429fd8b View commit details
    Browse the repository at this point in the history

  6. hI as separate lemma

    @winstonyin
    winstonyin committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    d1a8296 View commit details
    Browse the repository at this point in the history

  7. actually compiles

    @winstonyin
    winstonyin committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    7f7a49d View commit details
    Browse the repository at this point in the history

  8. minor

    @winstonyin
    winstonyin committed Nov 26, 2023
    Configuration menu
    Copy the full SHA
    ab30700 View commit details
    Browse the repository at this point in the history

Commits on Nov 27, 2023

  1. Prefer refine over refine' in new code, per zulip. 

    And combine some apply lines.
    @grunweg
    grunweg committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    98ff512 View commit details
    Browse the repository at this point in the history

  2. Use mfld_simps to make proofs more readable. 

    Golf proofs about composition of integral curves.
    @grunweg
    grunweg committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    00f4e77 View commit details
    Browse the repository at this point in the history

  3. Small golf, use mfld_simps more.

    @grunweg
    grunweg committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    e86759d View commit details
    Browse the repository at this point in the history

  4. hasFDerivWithinAt_tangentCoordChange

    @winstonyin
    winstonyin committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    85fbe5d View commit details
    Browse the repository at this point in the history

Commits on Nov 28, 2023

  1. some golf

    @winstonyin
    winstonyin committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    d924890 View commit details
    Browse the repository at this point in the history

  2. shorten comment

    @winstonyin
    winstonyin committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    4cf8097 View commit details
    Browse the repository at this point in the history

  3. shorten

    @winstonyin
    winstonyin committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    e8bfdb0 View commit details
    Browse the repository at this point in the history

  4. move tangentCoordChange

    @winstonyin
    winstonyin committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    de44a9c View commit details
    Browse the repository at this point in the history

  5. minor spacing

    @winstonyin
    winstonyin committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    a792394 View commit details
    Browse the repository at this point in the history

  6. isIntegralCurveAt_const

    @winstonyin
    winstonyin committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    4cc6c69 View commit details
    Browse the repository at this point in the history

  7. remove todo

    @winstonyin
    winstonyin committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    b4ba5a0 View commit details
    Browse the repository at this point in the history

  8. use implicit lambdas

    @winstonyin
    winstonyin committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    f14affa View commit details
    Browse the repository at this point in the history

Commits on Nov 29, 2023

  1. Fix style.

    @grunweg
    grunweg committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    0a3d359 View commit details
    Browse the repository at this point in the history

  2. Remove superfluous helper lemma.

    @grunweg
    grunweg committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    fa1b5f3 View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2023

  1. docstring, rename theorem

    @winstonyin
    winstonyin committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    9e9ee92 View commit details
    Browse the repository at this point in the history

  2. rename

    @winstonyin
    winstonyin committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    75c2b52 View commit details
    Browse the repository at this point in the history

  3. remove x₀ from IsIntegralCurveAt

    @winstonyin
    winstonyin committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    f019e9b View commit details
    Browse the repository at this point in the history

  4. end with exact

    @winstonyin
    winstonyin committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    30c333f View commit details
    Browse the repository at this point in the history

  5. IsIntegralCurveOn, IsIntegralCurve

    @winstonyin
    winstonyin committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    e140c43 View commit details
    Browse the repository at this point in the history

  6. docstring

    @winstonyin
    winstonyin committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    b810d2a View commit details
    Browse the repository at this point in the history

  7. IsIntegralCurveAt.isIntegralCurveOn

    @winstonyin
    winstonyin committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    9f5b559 View commit details
    Browse the repository at this point in the history

  8. comp_add lemmas

    @winstonyin
    winstonyin committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    0445938 View commit details
    Browse the repository at this point in the history

  9. refactored IsIntegralCurveXX

    @winstonyin
    winstonyin committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    3b7cca0 View commit details
    Browse the repository at this point in the history

  10. unused arg

    @winstonyin
    winstonyin committed Nov 30, 2023
    Configuration menu
    Copy the full SHA
    082574b View commit details
    Browse the repository at this point in the history

Commits on Dec 1, 2023

  1. statement

    @winstonyin
    winstonyin committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    ac90345 View commit details
    Browse the repository at this point in the history

  2. gronwall LipschitzOnWith

    @winstonyin
    winstonyin committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    19a2e81 View commit details
    Browse the repository at this point in the history

  3. partial

    @winstonyin
    winstonyin committed Dec 1, 2023
    Configuration menu
    Copy the full SHA
    b08e243 View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2023

  1. some corollaries in Gronwall

    @winstonyin
    winstonyin committed Dec 4, 2023
    Configuration menu
    Copy the full SHA
    08d1e12 View commit details
    Browse the repository at this point in the history

Commits on Dec 5, 2023

  1. Ioo version

    @winstonyin
    winstonyin committed Dec 5, 2023
    Configuration menu
    Copy the full SHA
    f80b337 View commit details
    Browse the repository at this point in the history

Commits on Dec 6, 2023

  1. stuck

    @winstonyin
    winstonyin committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    49c5acb View commit details
    Browse the repository at this point in the history

  2. can't believe it compiles lol

    @winstonyin
    winstonyin committed Dec 6, 2023
    Configuration menu
    Copy the full SHA
    e52f2ff View commit details
    Browse the repository at this point in the history

Commits on Dec 7, 2023

  1. draft

    @winstonyin
    winstonyin committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    5e4df2a View commit details
    Browse the repository at this point in the history

  2. uniqueness sorry-free!

    @winstonyin
    winstonyin committed Dec 7, 2023
    Configuration menu
    Copy the full SHA
    33d9a79 View commit details
    Browse the repository at this point in the history

Commits on Dec 8, 2023

  1. docstring

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    f22da92 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into integral_curve

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    fbb74c9 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'integral_curve' into unique_integral_curve

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    5607d5a View commit details
    Browse the repository at this point in the history

  4. space

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    a9d4cae View commit details
    Browse the repository at this point in the history

  5. Merge branch 'integral_curve' into unique_integral_curve

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    9d54e62 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin/master' into unique_integral_curve

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    0249431 View commit details
    Browse the repository at this point in the history

  7. shorten

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    860f52f View commit details
    Browse the repository at this point in the history

  8. shorten

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    d6d70f5 View commit details
    Browse the repository at this point in the history

  9. unused

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    6ea9338 View commit details
    Browse the repository at this point in the history

  10. Small things: sectioning; re-use variables.

    @grunweg
    grunweg committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    6d4af73 View commit details
    Browse the repository at this point in the history

  11. Tinygolf.

    @grunweg
    grunweg committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    ffa3c4b View commit details
    Browse the repository at this point in the history

  12. Line breaks.

    @grunweg
    grunweg committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    7dde305 View commit details
    Browse the repository at this point in the history

  13. golf a bit

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    b6a1ada View commit details
    Browse the repository at this point in the history

  14. golf and docstring

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    f5f7f70 View commit details
    Browse the repository at this point in the history

  15. usued args

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    4b2a738 View commit details
    Browse the repository at this point in the history

  16. remove temp notation

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    1898133 View commit details
    Browse the repository at this point in the history

  17. oops

    @winstonyin
    winstonyin committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    fa1e07f View commit details
    Browse the repository at this point in the history

Commits on Dec 9, 2023

  1. small golf

    @winstonyin
    winstonyin committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    780373e View commit details
    Browse the repository at this point in the history

  2. EqOn

    @winstonyin
    winstonyin committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    8cfee4c View commit details
    Browse the repository at this point in the history

  3. style

    @winstonyin
    winstonyin committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    64942d1 View commit details
    Browse the repository at this point in the history

  4. style

    @winstonyin
    winstonyin committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    cb2fab2 View commit details
    Browse the repository at this point in the history

  5. have parentheses

    @winstonyin
    winstonyin committed Dec 9, 2023
    Configuration menu
    Copy the full SHA
    3a6a98d View commit details
    Browse the repository at this point in the history

Commits on Dec 13, 2023

  1. style

    @winstonyin
    winstonyin committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    06674b3 View commit details
    Browse the repository at this point in the history

  2. fix

    @winstonyin
    winstonyin committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    5c5f070 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'integral_curve' into unique_integral_curve

    @winstonyin
    winstonyin committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    71d1021 View commit details
    Browse the repository at this point in the history

  4. style

    @winstonyin
    winstonyin committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    ccd1830 View commit details
    Browse the repository at this point in the history

  5. spacing

    @winstonyin
    winstonyin committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    122546d View commit details
    Browse the repository at this point in the history

  6. spacing

    @winstonyin
    winstonyin committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    c1c57c9 View commit details
    Browse the repository at this point in the history

  7. split aux lemmas out

    @winstonyin
    winstonyin committed Dec 13, 2023
    Configuration menu
    Copy the full SHA
    0ed0eec View commit details
    Browse the repository at this point in the history

Commits on Dec 14, 2023

  1. refactored with shrinkable

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    729d547 View commit details
    Browse the repository at this point in the history

  2. use filters, eventually

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    5e45ca2 View commit details
    Browse the repository at this point in the history

  3. all using filters now

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    842284d View commit details
    Browse the repository at this point in the history

  4. style

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    abbcbd8 View commit details
    Browse the repository at this point in the history

  5. doc

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    8d91420 View commit details
    Browse the repository at this point in the history

  6. restate existence theorem using filters

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    2c4d77d View commit details
    Browse the repository at this point in the history

  7. define IsIntegralCurveAt using Eventually

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    5f7bb14 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'integral_curve' into unique_integral_curve

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    182c699 View commit details
    Browse the repository at this point in the history

  9. Merge remote-tracking branch 'origin/master' into unique_integral_curve

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    eec9c85 View commit details
    Browse the repository at this point in the history

  10. Merge remote-tracking branch 'origin/master' into integral_curve

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    29170c6 View commit details
    Browse the repository at this point in the history

  11. PartialEquiv

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    6341072 View commit details
    Browse the repository at this point in the history

  12. PartialEquiv

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    7911121 View commit details
    Browse the repository at this point in the history

  13. PartialEquiv

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    8e54212 View commit details
    Browse the repository at this point in the history

  14. PartialEquiv

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    7b1bc43 View commit details
    Browse the repository at this point in the history

  15. PartialEquiv

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    4efc1ad View commit details
    Browse the repository at this point in the history

  16. Partial

    @winstonyin
    winstonyin committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    2508953 View commit details
    Browse the repository at this point in the history

  17. Replace => by \mapsto, per the style guide.

    @grunweg
    grunweg committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    7b804f9 View commit details
    Browse the repository at this point in the history

  18. Small golfs.

    @grunweg
    grunweg committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    22d5ceb View commit details
    Browse the repository at this point in the history

Commits on Dec 15, 2023

  1. small golf

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    c4dd6bc View commit details
    Browse the repository at this point in the history

  2. congr_deriv

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    d32e895 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/congr_deriv' into unique_integra… 

    …l_curve
    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    7dead4d View commit details
    Browse the repository at this point in the history

  4. use new lemmas

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    fff3d19 View commit details
    Browse the repository at this point in the history

  5. missed one

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    4559d57 View commit details
    Browse the repository at this point in the history

  6. fderiv -> deriv

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    17cb91b View commit details
    Browse the repository at this point in the history

  7. congr_mfderiv

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    8712cb8 View commit details
    Browse the repository at this point in the history

  8. mfderiv_chartAt_eq_tangentCoordChange

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    d4c5b05 View commit details
    Browse the repository at this point in the history

  9. golf

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    a5c75c1 View commit details
    Browse the repository at this point in the history

  10. uncomment

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    f17b87d View commit details
    Browse the repository at this point in the history

  11. reorder

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    9acde4a View commit details
    Browse the repository at this point in the history

  12. implicit variables

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    fa459a5 View commit details
    Browse the repository at this point in the history

  13. Merge branch 'integral_curve' into unique_integral_curve

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    850ab35 View commit details
    Browse the repository at this point in the history

  14. implicit variable

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    e34a30a View commit details
    Browse the repository at this point in the history

  15. organise variables, docstring

    @winstonyin
    winstonyin committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    3ba365f View commit details
    Browse the repository at this point in the history

Commits on Dec 16, 2023

  1. Merge remote-tracking branch 'origin/master' into unique_integral_curve

    @winstonyin
    winstonyin committed Dec 16, 2023
    Configuration menu
    Copy the full SHA
    9cb4fb6 View commit details
    Browse the repository at this point in the history

Commits on Dec 17, 2023

  1. Update Mathlib/Geometry/Manifold/IntegralCurve.lean 

    Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
    @winstonyin @thorimur
    winstonyin and thorimur committed Dec 17, 2023
    Configuration menu
    Copy the full SHA
    e784d93 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Geometry/Manifold/IntegralCurve.lean 

    Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
    @winstonyin @thorimur
    winstonyin and thorimur committed Dec 17, 2023
    Configuration menu
    Copy the full SHA
    47e137d View commit details
    Browse the repository at this point in the history

Commits on Dec 18, 2023

  1. Update Mathlib/Geometry/Manifold/IntegralCurve.lean 

    Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
    @winstonyin @thorimur
    winstonyin and thorimur committed Dec 18, 2023
    Configuration menu
    Copy the full SHA
    2e0b9bf View commit details
    Browse the repository at this point in the history

  2. remove newlines

    @winstonyin
    winstonyin committed Dec 18, 2023
    Configuration menu
    Copy the full SHA
    26be30a View commit details
    Browse the repository at this point in the history

Commits on Dec 19, 2023

  1. Merge remote-tracking branch 'origin/master' into integral_curve

    @winstonyin
    winstonyin committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    90755c3 View commit details
    Browse the repository at this point in the history

  2. fix

    @winstonyin
    winstonyin committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    5aab426 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'integral_curve' into unique_integral_curve

    @winstonyin
    winstonyin committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    020e07b View commit details
    Browse the repository at this point in the history

Commits on Dec 20, 2023

  1. fix

    @winstonyin
    winstonyin committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    1ea3813 View commit details
    Browse the repository at this point in the history

Commits on Dec 29, 2023

  1. IsIntegralCurveAt.hasMFDerivAt

    @winstonyin
    winstonyin committed Dec 29, 2023
    Configuration menu
    Copy the full SHA
    749ea8c View commit details
    Browse the repository at this point in the history

  2. Merge branch 'integral_curve' into unique_integral_curve

    @winstonyin
    winstonyin committed Dec 29, 2023
    Configuration menu
    Copy the full SHA
    3c41d58 View commit details
    Browse the repository at this point in the history

  3. statement

    @winstonyin
    winstonyin committed Dec 29, 2023
    Configuration menu
    Copy the full SHA
    4a735d2 View commit details
    Browse the repository at this point in the history

Commits on Dec 30, 2023

  1. compiles

    @winstonyin
    winstonyin committed Dec 30, 2023
    Configuration menu
    Copy the full SHA
    12369b4 View commit details
    Browse the repository at this point in the history

  2. restate as iff

    @winstonyin
    winstonyin committed Dec 30, 2023
    Configuration menu
    Copy the full SHA
    3acfc7f View commit details
    Browse the repository at this point in the history

  3. lemma

    @winstonyin
    winstonyin committed Dec 30, 2023
    Configuration menu
    Copy the full SHA
    0bb45eb View commit details
    Browse the repository at this point in the history

Commits on Jan 5, 2024

  1. Merge remote-tracking branch 'origin/master' into integral_curve

    @winstonyin
    winstonyin committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    ca88b9d View commit details
    Browse the repository at this point in the history

  2. Merge branch 'integral_curve' into unique_integral_curve

    @winstonyin
    winstonyin committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    e06f50b View commit details
    Browse the repository at this point in the history

  3. Merge branch 'unique_integral_curve' into integral_curve_injective

    @winstonyin
    winstonyin committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    a90f105 View commit details
    Browse the repository at this point in the history

  4. BoundarylessManifold

    @winstonyin
    winstonyin committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    c74e830 View commit details
    Browse the repository at this point in the history

  5. BoundarylessManifold

    @winstonyin
    winstonyin committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    ec1df62 View commit details
    Browse the repository at this point in the history

  6. BoundarylessManifold

    @winstonyin
    winstonyin committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    9db3abf View commit details
    Browse the repository at this point in the history

  7. Merge branch 'unique_integral_curve' into integral_curve_injective

    @winstonyin
    winstonyin committed Jan 5, 2024
    Configuration menu
    Copy the full SHA
    8511979 View commit details
    Browse the repository at this point in the history

Commits on Jan 8, 2024

  1. Make I implicit again.

    @grunweg
    grunweg committed Jan 8, 2024
    Configuration menu
    Copy the full SHA
    353f3c9 View commit details
    Browse the repository at this point in the history

  2. Open Function: mostly for Function.comp_apply.

    @grunweg
    grunweg committed Jan 8, 2024
    Configuration menu
    Copy the full SHA
    a0c398b View commit details
    Browse the repository at this point in the history

  3. Extract one direction into a lemma.

    @grunweg
    grunweg committed Jan 8, 2024
    Configuration menu
    Copy the full SHA
    8461f75 View commit details
    Browse the repository at this point in the history

  4. Add xor version; tweak lemma name.

    @grunweg
    grunweg committed Jan 8, 2024
    Configuration menu
    Copy the full SHA
    ba3dd3a View commit details
    Browse the repository at this point in the history

  5. docs, golf, add isIntegralCurveOn_iff_isIntegralCurveAt

    @winstonyin
    winstonyin committed Jan 8, 2024
    Configuration menu
    Copy the full SHA
    7d7a716 View commit details
    Browse the repository at this point in the history

  6. use Eventually in IsIntegralCurveAt

    @winstonyin
    winstonyin committed Jan 8, 2024
    Configuration menu
    Copy the full SHA
    db893bd View commit details
    Browse the repository at this point in the history

  7. minor

    @winstonyin
    winstonyin committed Jan 8, 2024
    Configuration menu
    Copy the full SHA
    ad6d0a6 View commit details
    Browse the repository at this point in the history

Commits on Jan 9, 2024

  1. Merge branch 'integral_curve' into unique_integral_curve

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    e9eaec2 View commit details
    Browse the repository at this point in the history

  2. fix

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    5c7eca6 View commit details
    Browse the repository at this point in the history

  3. golf

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    fed6c68 View commit details
    Browse the repository at this point in the history

  4. golf

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    89e0297 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/master' into unique_integral_curve

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    8f0b80a View commit details
    Browse the repository at this point in the history

  6. golf some earlier proofs

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    a00ed88 View commit details
    Browse the repository at this point in the history

  7. minor

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    8493b01 View commit details
    Browse the repository at this point in the history

  8. doc

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    15f7e4f View commit details
    Browse the repository at this point in the history

  9. Merge branch 'unique_integral_curve' into integral_curve_injective

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    cf77f13 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'integral_curve_injective' of https://github.com/leanpro… 

    …ver-community/mathlib4 into integral_curve_injective
    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    cd321af View commit details
    Browse the repository at this point in the history

  11. section header

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    1c91b79 View commit details
    Browse the repository at this point in the history

  12. docs

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    212b12d View commit details
    Browse the repository at this point in the history

  13. Merge branch 'unique_integral_curve' into integral_curve_injective

    @winstonyin
    winstonyin committed Jan 9, 2024
    Configuration menu
    Copy the full SHA
    f10e247 View commit details
    Browse the repository at this point in the history

Commits on Jan 11, 2024

  1. typo

    @winstonyin
    winstonyin committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    fbd2199 View commit details
    Browse the repository at this point in the history

Commits on Jan 15, 2024

  1. Merge remote-tracking branch 'origin/master' into unique_integral_curve

    @winstonyin
    winstonyin committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    4ef4954 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into integral_curve_inje… 

    …ctive
    @winstonyin
    winstonyin committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    bb3e5b7 View commit details
    Browse the repository at this point in the history

Commits on Jan 17, 2024

  1. Merge remote-tracking branch 'origin/master' into unique_integral_curve

    @winstonyin
    winstonyin committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    eb40505 View commit details
    Browse the repository at this point in the history

  2. fix

    @winstonyin
    winstonyin committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    a889e9f View commit details
    Browse the repository at this point in the history

  3. gronwall doc

    @winstonyin
    winstonyin committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    a44856a View commit details
    Browse the repository at this point in the history

  4. minor

    @winstonyin
    winstonyin committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    92df5b9 View commit details
    Browse the repository at this point in the history

  5. move lemma

    @winstonyin
    winstonyin committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    06d6fa4 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'unique_integral_curve' into integral_curve_injective

    @winstonyin
    winstonyin committed Jan 17, 2024
    Configuration menu
    Copy the full SHA
    595c63e View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2024

  1. Merge remote-tracking branch 'origin/master' into integral_curve_inje… 

    …ctive
    @winstonyin
    winstonyin committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    a489cf5 View commit details
    Browse the repository at this point in the history

  2. fix

    @winstonyin
    winstonyin committed Jan 24, 2024
    Configuration menu
    Copy the full SHA
    4a3f868 View commit details
    Browse the repository at this point in the history

Commits on Jan 29, 2024

  1. rewrite

    @winstonyin
    winstonyin committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    de220be View commit details
    Browse the repository at this point in the history

  2. AddZeroClass

    @winstonyin
    winstonyin committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    1b5e97b View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into integral_curve_injective

    @urkud
    urkud committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    d39c4eb View commit details
    Browse the repository at this point in the history

  4. Golf, fix docstring

    @urkud
    urkud committed Jan 29, 2024
    Configuration menu
    Copy the full SHA
    e8a02c6 View commit details
    Browse the repository at this point in the history