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

feat(RingTheory.MvPowerSeries.Topology): define the product topology on mv power series #14866

Open
wants to merge 82 commits into
base: master
Choose a base branch
from
Open

feat(RingTheory.MvPowerSeries.Topology): define the product topology on mv power series #14866

wants to merge 82 commits into from
+463 −0

Commits on Jul 18, 2024

  1. coefficients of powers of MvPowerSeries

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    7cb1908 View commit details
    Browse the repository at this point in the history

  2. initial commit

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    bdef1b0 View commit details
    Browse the repository at this point in the history

  3. update references.bib

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    06c9528 View commit details
    Browse the repository at this point in the history

  4. delete one blank line

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    543b97f View commit details
    Browse the repository at this point in the history

  5. Merge branch 'ACLMIdFF/MvPowerSeries_coeffpow' into ACLMIdFF/MvPowerS… 

    …eries_Topology
    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    c2c4976 View commit details
    Browse the repository at this point in the history

  6. defines the topology (removes homogeneous components)

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    3d5a7d0 View commit details
    Browse the repository at this point in the history

  7. correct def to theorem

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    2649640 View commit details
    Browse the repository at this point in the history

  8. update

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    8345665 View commit details
    Browse the repository at this point in the history

  9. mention non-relation with adic topology

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    805f1d5 View commit details
    Browse the repository at this point in the history

  10. correct centered dots

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    54bbcea View commit details
    Browse the repository at this point in the history

  11. update Mathlib.lean

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    8d001f7 View commit details
    Browse the repository at this point in the history

  12. make lint happy (try to)

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    d507e68 View commit details
    Browse the repository at this point in the history

  13. update

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    1191b60 View commit details
    Browse the repository at this point in the history

  14. move weights to other file

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    cb8c681 View commit details
    Browse the repository at this point in the history

  15. homogeneize

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    5820cc0 View commit details
    Browse the repository at this point in the history

  16. adjust for degrees

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    6e26559 View commit details
    Browse the repository at this point in the history

  17. add le_degree

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    aae13ce View commit details
    Browse the repository at this point in the history

  18. update mathlib.lean

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    df1d019 View commit details
    Browse the repository at this point in the history

  19. try to make lint happy

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    b2bbb36 View commit details
    Browse the repository at this point in the history

  20. adjust

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    f649884 View commit details
    Browse the repository at this point in the history

  21. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    4831b9b View commit details
    Browse the repository at this point in the history

  22. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    bdfe910 View commit details
    Browse the repository at this point in the history

  23. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    bafb2d7 View commit details
    Browse the repository at this point in the history

  24. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    d744b9a View commit details
    Browse the repository at this point in the history

  25. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    bc296a4 View commit details
    Browse the repository at this point in the history

  26. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    93df652 View commit details
    Browse the repository at this point in the history

  27. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @AntoineChambert-Loir @github-actions
    AntoineChambert-Loir and github-actions[bot] authored Jul 18, 2024
    Configuration menu
    Copy the full SHA
    da2b237 View commit details
    Browse the repository at this point in the history

  28. apply (almost all of) Filippo's comments

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    c6886c7 View commit details
    Browse the repository at this point in the history

  29. adjust

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    a2049f3 View commit details
    Browse the repository at this point in the history

  30. adjust and simplify

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    e7c89bd View commit details
    Browse the repository at this point in the history

  31. make a def a theorem

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    165e928 View commit details
    Browse the repository at this point in the history

  32. add a docstring

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    3a0ec1e View commit details
    Browse the repository at this point in the history

  33. adjust to import - linter

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    4ecd44c View commit details
    Browse the repository at this point in the history

  34. adjust scoped instances following linter

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    8dea296 View commit details
    Browse the repository at this point in the history

  35. adjust import

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    e0eb0fb View commit details
    Browse the repository at this point in the history

  36. adjust import

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    63924ca View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2024

  1. Merge branch 'master' into ACLMIdFF/degree

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    72f8dce View commit details
    Browse the repository at this point in the history

  2. remove all #align and #align_import

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    521492a View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 19, 2024
    Configuration menu
    Copy the full SHA
    3054cbb View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 19, 2024
    Configuration menu
    Copy the full SHA
    ab06f0f View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 19, 2024
    Configuration menu
    Copy the full SHA
    ecade7c View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 19, 2024
    Configuration menu
    Copy the full SHA
    c82153a View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 19, 2024
    Configuration menu
    Copy the full SHA
    94ea8bf View commit details
    Browse the repository at this point in the history

  8. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 19, 2024
    Configuration menu
    Copy the full SHA
    c3e9092 View commit details
    Browse the repository at this point in the history

  9. Update Mathlib/RingTheory/MvPowerSeries/Basic.lean 

    Co-authored-by: Filippo A. E. Nuccio <[email protected]>
    @AntoineChambert-Loir @faenuccio
    AntoineChambert-Loir and faenuccio authored Jul 19, 2024
    Configuration menu
    Copy the full SHA
    54dafe5 View commit details
    Browse the repository at this point in the history

  10. adjust

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    6758185 View commit details
    Browse the repository at this point in the history

  11. linter 100

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    9123cf2 View commit details
    Browse the repository at this point in the history

Commits on Jul 20, 2024

  1. Merge branch 'ACLMIdFF/degree' into ACLMIdFF/MvPowerSeries_coeffpow

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    f1f83c1 View commit details
    Browse the repository at this point in the history

  2. adjust

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    761bbcf View commit details
    Browse the repository at this point in the history

  3. make some arguments implicit

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    0d1c9d6 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'ACLMIdFF/degree' into ACLMIdFF/MvPowerSeries_coeffpow

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    b9da976 View commit details
    Browse the repository at this point in the history

  5. add docstring

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    c96c50c View commit details
    Browse the repository at this point in the history

  6. linter 100 / adjust

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 20, 2024
    Configuration menu
    Copy the full SHA
    0492feb View commit details
    Browse the repository at this point in the history

Commits on Jul 21, 2024

  1. Merge branch 'master' into ACLMIdFF/MvPowerSeries_coeffpow

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 21, 2024
    Configuration menu
    Copy the full SHA
    c2d9b6f View commit details
    Browse the repository at this point in the history

  2. change refine' to apply

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 21, 2024
    Configuration menu
    Copy the full SHA
    48d2f35 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'ACLMIdFF/MvPowerSeries_coeffpow' into ACLMIdFF/MvPowerS… 

    …eries_Topology
    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 21, 2024
    Configuration menu
    Copy the full SHA
    13cb3b2 View commit details
    Browse the repository at this point in the history

  4. adjust

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 21, 2024
    Configuration menu
    Copy the full SHA
    d167eb3 View commit details
    Browse the repository at this point in the history

  5. better docstring

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 21, 2024
    Configuration menu
    Copy the full SHA
    8d7a099 View commit details
    Browse the repository at this point in the history

  6. better preamble

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 21, 2024
    Configuration menu
    Copy the full SHA
    c21f5dd View commit details
    Browse the repository at this point in the history

  7. linter 100

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 21, 2024
    Configuration menu
    Copy the full SHA
    f46bac1 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2024

  1. change α to R

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    ddd42b9 View commit details
    Browse the repository at this point in the history

  2. answer JC's comments + some lemmas hold more generally

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    3a3dbf4 View commit details
    Browse the repository at this point in the history

  3. linter 100

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    082d250 View commit details
    Browse the repository at this point in the history

  4. generalize

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    19944af View commit details
    Browse the repository at this point in the history

Commits on Jul 29, 2024

  1. Merge branch 'master' into ACLMIdFF/MvPowerSeries_Topology

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    9bf21d8 View commit details
    Browse the repository at this point in the history

  2. rename Topology to PiTopology

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    d03c51f View commit details
    Browse the repository at this point in the history

  3. mv stuff to BigOperators and change apply_eq_coeff

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    62170fe View commit details
    Browse the repository at this point in the history

  4. never consider power series as functions

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    0493cf1 View commit details
    Browse the repository at this point in the history

  5. cleanup, docstrings

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    379fbca View commit details
    Browse the repository at this point in the history

  6. add PowerSeries/PiTopology

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    d0cf16b View commit details
    Browse the repository at this point in the history

  7. correct class

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    e6e52e8 View commit details
    Browse the repository at this point in the history

Commits on Sep 6, 2024

  1. use Pi instances, reorder file

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Sep 6, 2024
    Configuration menu
    Copy the full SHA
    71ed0cc View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2024

  1. fix namespaces

    @mariainesdff
    mariainesdff committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    b369662 View commit details
    Browse the repository at this point in the history

  2. expand comments

    @mariainesdff
    mariainesdff committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    5d19e4d View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2024

  1. Update Mathlib/RingTheory/MvPowerSeries/PiTopology.lean 

    Co-authored-by: Johan Commelin <[email protected]>
    @AntoineChambert-Loir @jcommelin
    AntoineChambert-Loir and jcommelin authored Sep 20, 2024
    Configuration menu
    Copy the full SHA
    c6faa8a View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/RingTheory/PowerSeries/PiTopology.lean 

    Co-authored-by: Johan Commelin <[email protected]>
    @AntoineChambert-Loir @jcommelin
    AntoineChambert-Loir and jcommelin authored Sep 20, 2024
    Configuration menu
    Copy the full SHA
    13fa966 View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/RingTheory/MvPowerSeries/PiTopology.lean 

    Co-authored-by: Johan Commelin <[email protected]>
    @AntoineChambert-Loir @jcommelin
    AntoineChambert-Loir and jcommelin authored Sep 20, 2024
    Configuration menu
    Copy the full SHA
    3546540 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/RingTheory/MvPowerSeries/PiTopology.lean 

    Co-authored-by: Johan Commelin <[email protected]>
    @AntoineChambert-Loir @jcommelin
    AntoineChambert-Loir and jcommelin authored Sep 20, 2024
    Configuration menu
    Copy the full SHA
    596670e View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/RingTheory/MvPowerSeries/PiTopology.lean 

    Co-authored-by: Johan Commelin <[email protected]>
    @AntoineChambert-Loir @jcommelin
    AntoineChambert-Loir and jcommelin authored Sep 20, 2024
    Configuration menu
    Copy the full SHA
    a817bc3 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/RingTheory/MvPowerSeries/PiTopology.lean 

    Co-authored-by: Johan Commelin <[email protected]>
    @AntoineChambert-Loir @jcommelin
    AntoineChambert-Loir and jcommelin authored Sep 20, 2024
    Configuration menu
    Copy the full SHA
    8212c6d View commit details
    Browse the repository at this point in the history

  7. remove variable declaration and DecidableEq assumption

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    054ea42 View commit details
    Browse the repository at this point in the history

  8. add classical

    @AntoineChambert-Loir
    AntoineChambert-Loir committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    57fce93 View commit details
    Browse the repository at this point in the history