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(GroupTheory/Archimedean): LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered #15846

Closed
wants to merge 72 commits into from
Closed

[Merged by Bors] - feat(GroupTheory/Archimedean): LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered #15846

wants to merge 72 commits into from

Commits on Aug 7, 2024

  1. feat(Algebra/Order/Archimedean): multiplicativize Archimedean 

    This allows one to talk about finding powers greater than some element for ordered monoids
Before, this was only available for ordered semirings
This is to later installthe instance on valuation groups (`LinearOrderedCommGroupWithZero`)
Install the instance on NNRat and NNReal (though they are ordered semirings)
Also, add some misisng instances about the nonnegative submonoid
    @pechersky
    pechersky committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    dbba7e9 View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2024

  1. feat(GroupTheory/Archimedean): `LinearOrderedAddCommGroup.discrete_or… 

    …_denselyOrdered`

Classfy linearly ordered additive groups, either they are discrete (order isomorphic to Int) or densely ordered
Also add some simple lemmas about the closure subgroup.
    @pechersky
    pechersky committed Aug 9, 2024
    Configuration menu
    Copy the full SHA
    b1e8032 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into pechersky/mul-archimedean

    @pechersky
    pechersky committed Aug 9, 2024
    Configuration menu
    Copy the full SHA
    4ab710a View commit details
    Browse the repository at this point in the history

  3. left arrow

    @pechersky
    pechersky committed Aug 9, 2024
    Configuration menu
    Copy the full SHA
    0e57f15 View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2024

  1. unsimp, due to pointwise

    @pechersky
    pechersky committed Aug 11, 2024
    Configuration menu
    Copy the full SHA
    e039680 View commit details
    Browse the repository at this point in the history

  2. generalize closure equiv

    @pechersky
    pechersky committed Aug 11, 2024
    Configuration menu
    Copy the full SHA
    12d7a39 View commit details
    Browse the repository at this point in the history

Commits on Aug 13, 2024

  1. add additive docstring

    @pechersky
    pechersky committed Aug 13, 2024
    Configuration menu
    Copy the full SHA
    ca18efa View commit details
    Browse the repository at this point in the history

Commits on Aug 14, 2024

  1. Merge branch 'pechersky/mul-archimedean' into pechersky/multiplicativ… 

    …ize-group-archimedean
    @pechersky
    pechersky committed Aug 14, 2024
    Configuration menu
    Copy the full SHA
    a6c4566 View commit details
    Browse the repository at this point in the history

  2. feat(GroupTheory/Archimedean): multiplicativize

    @pechersky
    pechersky committed Aug 14, 2024
    Configuration menu
    Copy the full SHA
    d325a7b View commit details
    Browse the repository at this point in the history

Commits on Aug 15, 2024

  1. Merge branch 'pechersky/discrete-or-denselyOrdered' into pechersky/mu… 

    …ltiplicativize-group-archimedean
    @pechersky
    pechersky committed Aug 15, 2024
    Configuration menu
    Copy the full SHA
    363ee74 View commit details
    Browse the repository at this point in the history

  2. feat(GroupTheory/Archimedean): `LinearOrderedCommGroupWithZero.discre… 

    …te_or_denselyOrdered`

Along with helper equivs about `Units`
and some missing instances about `Units`.
    @pechersky
    pechersky committed Aug 15, 2024
    Configuration menu
    Copy the full SHA
    e733f83 View commit details
    Browse the repository at this point in the history

Commits on Aug 25, 2024

  1. feedback

    @pechersky
    pechersky committed Aug 25, 2024
    Configuration menu
    Copy the full SHA
    526e85e View commit details
    Browse the repository at this point in the history

  2. feedback

    @pechersky
    pechersky committed Aug 25, 2024
    Configuration menu
    Copy the full SHA
    a001674 View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2024

  1. feat(Algebra/Order/Hom): Order(Add)MonoidIso

    @pechersky
    pechersky committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    07a7465 View commit details
    Browse the repository at this point in the history

  2. bring instance back

    @pechersky
    pechersky committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    b049050 View commit details
    Browse the repository at this point in the history

  3. move to pointwise

    @pechersky
    pechersky committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    e5b8fcb View commit details
    Browse the repository at this point in the history

  4. change import

    @pechersky
    pechersky committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    f869164 View commit details
    Browse the repository at this point in the history

  5. fix naming

    @pechersky
    pechersky committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    876152d View commit details
    Browse the repository at this point in the history

Commits on Aug 27, 2024

  1. Update Mathlib/GroupTheory/Archimedean.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @pechersky @YaelDillies
    pechersky and YaelDillies authored Aug 27, 2024
    Configuration menu
    Copy the full SHA
    83d4c43 View commit details
    Browse the repository at this point in the history

  2. Revert "Update Mathlib/GroupTheory/Archimedean.lean" 

    This reverts commit 83d4c43.
    @pechersky
    pechersky committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    298c014 View commit details
    Browse the repository at this point in the history

Commits on Aug 28, 2024

  1. Update Mathlib/Algebra/Order/Hom/Monoid.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @pechersky @YaelDillies
    pechersky and YaelDillies authored Aug 28, 2024
    Configuration menu
    Copy the full SHA
    fe81ea6 View commit details
    Browse the repository at this point in the history

  2. docstring on parametrize over FunLike instead

    @pechersky
    pechersky committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    a35ae6e View commit details
    Browse the repository at this point in the history

  3. remove parens

    @pechersky
    pechersky committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    1639c05 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'pechersky/order-monoid-iso' into pechersky/discrete-or-… 

    …denselyOrdered
    @pechersky
    pechersky committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    b1be6b0 View commit details
    Browse the repository at this point in the history

  5. use ordermulequiv 

    moving lemma due to new variable
    @pechersky
    pechersky committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    47ce27c View commit details
    Browse the repository at this point in the history

  6. to_additive and generalize

    @pechersky
    pechersky committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    458be4e View commit details
    Browse the repository at this point in the history

  7. add zpow_right_inj/zsmul_left_inj and use it

    @pechersky
    pechersky committed Aug 28, 2024
    Configuration menu
    Copy the full SHA
    ec924b4 View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2024

  1. use orderAddIso

    @pechersky
    pechersky committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    48815d4 View commit details
    Browse the repository at this point in the history

  2. rename and use max

    @pechersky
    pechersky committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    1df8e6b View commit details
    Browse the repository at this point in the history

Commits on Aug 30, 2024

  1. Merge branch 'master' into pechersky/discrete-or-denselyOrdered

    @pechersky
    pechersky committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    5b51d52 View commit details
    Browse the repository at this point in the history

  2. fix proof

    @pechersky
    pechersky committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    dc414c2 View commit details
    Browse the repository at this point in the history

  3. fix again

    @pechersky
    pechersky committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    22e4b8a View commit details
    Browse the repository at this point in the history

Commits on Sep 1, 2024

  1. move closure_singleton_int_one_eq_top

    @pechersky
    pechersky committed Sep 1, 2024
    Configuration menu
    Copy the full SHA
    3f75390 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'pechersky/mul-archimedean' into pechersky/multiplicativ… 

    …ize-group-archimedean
    @pechersky
    pechersky committed Sep 1, 2024
    Configuration menu
    Copy the full SHA
    42e3914 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'pechersky/discrete-or-denselyOrdered' into pechersky/mu… 

    …ltiplicativize-group-archimedean
    @pechersky
    pechersky committed Sep 1, 2024
    Configuration menu
    Copy the full SHA
    08de427 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'pechersky/multiplicativize-group-archimedean' into pech… 

    …ersky/linear-ordered-comm-with-zero
    @pechersky
    pechersky committed Sep 1, 2024
    Configuration menu
    Copy the full SHA
    6852975 View commit details
    Browse the repository at this point in the history

  5. fix merge

    @pechersky
    pechersky committed Sep 1, 2024
    Configuration menu
    Copy the full SHA
    1d714e2 View commit details
    Browse the repository at this point in the history

  6. name instances better

    @pechersky
    pechersky committed Sep 1, 2024
    Configuration menu
    Copy the full SHA
    ced308a View commit details
    Browse the repository at this point in the history

  7. fix proofs

    @pechersky
    pechersky committed Sep 1, 2024
    Configuration menu
    Copy the full SHA
    e4c537b View commit details
    Browse the repository at this point in the history

  8. Merge branch 'pechersky/multiplicativize-group-archimedean' into pech… 

    …ersky/linear-ordered-comm-with-zero
    @pechersky
    pechersky committed Sep 1, 2024
    Configuration menu
    Copy the full SHA
    ac1d6be View commit details
    Browse the repository at this point in the history

  9. rewrite proofs

    @pechersky
    pechersky committed Sep 1, 2024
    Configuration menu
    Copy the full SHA
    bcbb8ae View commit details
    Browse the repository at this point in the history

  10. fix docstrings

    @pechersky
    pechersky committed Sep 1, 2024
    Configuration menu
    Copy the full SHA
    638e229 View commit details
    Browse the repository at this point in the history

Commits on Sep 2, 2024

  1. fix docstring

    @pechersky
    pechersky committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    51d926a View commit details
    Browse the repository at this point in the history

  2. actually use lemmas

    @pechersky
    pechersky committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    506bbc6 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'pechersky/discrete-or-denselyOrdered' into pechersky/mu… 

    …ltiplicativize-group-archimedean
    @pechersky
    pechersky committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    9b63e42 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'pechersky/multiplicativize-group-archimedean' into pech… 

    …ersky/linear-ordered-comm-with-zero
    @pechersky
    pechersky committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    08b1daf View commit details
    Browse the repository at this point in the history

Commits on Sep 8, 2024

  1. Merge branch 'master' into pechersky/multiplicativize-group-archimedean

    @pechersky
    pechersky committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    72f08b8 View commit details
    Browse the repository at this point in the history

  2. fix moves

    @pechersky
    pechersky committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    46c9cf2 View commit details
    Browse the repository at this point in the history

  3. remove empty line

    @pechersky
    pechersky committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    e8ff879 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'pechersky/multiplicativize-group-archimedean' into pech… 

    …ersky/linear-ordered-comm-with-zero
    @pechersky
    pechersky committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    7281608 View commit details
    Browse the repository at this point in the history

Commits on Sep 9, 2024

  1. feat(Algebra/GroupWithZero): MulEquiv between WithZero (units) and th… 

    …e base group with zero

Also MulEquivs that add or remove WithZero on both sides
And some basic WithOne/WithZero API
    @pechersky
    pechersky committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    df40fc7 View commit details
    Browse the repository at this point in the history

  2. feat(Algebra/Order/Units): LinearOrderedCommGroup Units when ambient … 

    …monoid is
    @pechersky
    pechersky committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    1bbee76 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'pechersky/units-locgw0' into pechersky/linear-ordered-c… 

    …omm-with-zero
    @pechersky
    pechersky committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    bfca2ed View commit details
    Browse the repository at this point in the history

  4. Merge branch 'pechersky/with-zero-congr' into pechersky/linear-ordere… 

    …d-comm-with-zero
    @pechersky
    pechersky committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    6f69b3b View commit details
    Browse the repository at this point in the history

  5. delete duplicate

    @pechersky
    pechersky committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    636c032 View commit details
    Browse the repository at this point in the history

  6. fix naming

    @pechersky
    pechersky committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    caa8340 View commit details
    Browse the repository at this point in the history

  7. signify that hypotheses will usually be found by unification

    @pechersky
    pechersky committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    7eff01a View commit details
    Browse the repository at this point in the history

  8. suggestions

    @pechersky
    pechersky committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    03cc550 View commit details
    Browse the repository at this point in the history

  9. suggestion

    @pechersky
    pechersky committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    6d9d415 View commit details
    Browse the repository at this point in the history

Commits on Sep 10, 2024

  1. tidy

    @pechersky
    pechersky committed Sep 10, 2024
    Configuration menu
    Copy the full SHA
    9900ba2 View commit details
    Browse the repository at this point in the history

Commits on Sep 12, 2024

  1. Merge branch 'master' into pechersky/linear-ordered-comm-with-zero

    @pechersky
    pechersky committed Sep 12, 2024
    Configuration menu
    Copy the full SHA
    2eaa7ec View commit details
    Browse the repository at this point in the history

  2. tidy more

    @pechersky
    pechersky committed Sep 12, 2024
    Configuration menu
    Copy the full SHA
    ad6d1f6 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'pechersky/with-zero-congr' into pechersky/linear-ordere… 

    …d-comm-with-zero
    @pechersky
    pechersky committed Sep 12, 2024
    Configuration menu
    Copy the full SHA
    8ad50ca View commit details
    Browse the repository at this point in the history

  4. fix names

    @pechersky
    pechersky committed Sep 12, 2024
    Configuration menu
    Copy the full SHA
    7cbb4c0 View commit details
    Browse the repository at this point in the history

Commits on Sep 15, 2024

  1. golf

    @pechersky
    pechersky committed Sep 15, 2024
    Configuration menu
    Copy the full SHA
    06bea0c View commit details
    Browse the repository at this point in the history

Commits on Sep 16, 2024

  1. Merge branch 'master' into pechersky/linear-ordered-comm-with-zero

    @pechersky
    pechersky committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    8e2fcea View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Algebra/Order/Archimedean/Basic.lean 

    Co-authored-by: Yaël Dillies <[email protected]>
    @pechersky @YaelDillies
    pechersky and YaelDillies authored Sep 16, 2024
    Configuration menu
    Copy the full SHA
    c2d498f View commit details
    Browse the repository at this point in the history

  3. notation

    @pechersky
    pechersky committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    4e54518 View commit details
    Browse the repository at this point in the history

  4. chore(GroupWitZero): more ℤₘ₀ earlier

    @pechersky
    pechersky committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    6c7142e View commit details
    Browse the repository at this point in the history

  5. remove DiscreteValuation notation duplicate

    @pechersky
    pechersky committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    ba57198 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'pechersky/zm0-notation' into pechersky/linear-ordered-c… 

    …omm-with-zero
    @pechersky
    pechersky committed Sep 16, 2024
    Configuration menu
    Copy the full SHA
    a585157 View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2024

  1. Merge branch 'master' into pechersky/linear-ordered-comm-with-zero

    @pechersky
    pechersky committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    3db831a View commit details
    Browse the repository at this point in the history