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(field_theory/ratfunc): rational functions as Laurent series #11276

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat(field_theory/ratfunc): rational functions as Laurent series #11276

wants to merge 28 commits into from

Commits on Jan 5, 2022

  1. feat(ring_theory/power_series/basic): algebra, solving TODOs

    @pechersky
    pechersky committed Jan 5, 2022
    Copy the full SHA
    4a9d313 View commit details
    Browse the repository at this point in the history

  2. initial change

    @pechersky
    pechersky committed Jan 5, 2022
    Copy the full SHA
    22afcb2 View commit details
    Browse the repository at this point in the history

Commits on Jan 6, 2022

  1. feat(algebra/*): injective hom into kernel map_eq_*_iff

    @pechersky
    pechersky committed Jan 6, 2022
    Copy the full SHA
    0a2d000 View commit details
    Browse the repository at this point in the history

  2. feat(field_theory/ratfunc): rational functions as Laurent series

    @pechersky
    pechersky committed Jan 6, 2022
    Copy the full SHA
    b0b4908 View commit details
    Browse the repository at this point in the history

  3. some things have explicit arguments

    @pechersky
    pechersky committed Jan 6, 2022
    Copy the full SHA
    b46241c View commit details
    Browse the repository at this point in the history

  4. Merge branch 'pechersky/hom-map-eq-iff' into pechersky/ratfunc-inj-la… 

    …urent-series
    @pechersky
    pechersky committed Jan 6, 2022
    Copy the full SHA
    d631342 View commit details
    Browse the repository at this point in the history

  5. missing import

    @pechersky
    pechersky committed Jan 6, 2022
    Copy the full SHA
    34d4da4 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'pechersky/power-series-algebra' into pechersky/ratfunc-… 

    …inj-laurent-series
    @pechersky
    pechersky committed Jan 6, 2022
    Copy the full SHA
    a0b92d7 View commit details
    Browse the repository at this point in the history

Commits on Jan 7, 2022

  1. feat(ring_theory/laurent): coercion of R[x] to R((x)) lemmas

    @pechersky
    pechersky committed Jan 7, 2022
    Copy the full SHA
    bb60725 View commit details
    Browse the repository at this point in the history

  2. feat(ring_theory/laurent): coercion of R[x] to R((x)) lemmas

    @pechersky
    pechersky committed Jan 7, 2022
    Copy the full SHA
    8429ddf View commit details
    Browse the repository at this point in the history

  3. finish coe to laurent

    @pechersky
    pechersky committed Jan 7, 2022
    Copy the full SHA
    ecf5c80 View commit details
    Browse the repository at this point in the history

  4. remove simp lemmas

    @pechersky
    pechersky committed Jan 7, 2022
    Copy the full SHA
    c6a7b93 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'pechersky/coe-laurent-poly' into pechersky/ratfunc-inj-… 

    …laurent-series
    @pechersky
    pechersky committed Jan 7, 2022
    Copy the full SHA
    ed49fd1 View commit details
    Browse the repository at this point in the history

  6. suggestion and cleaning, slay simp loop

    @pechersky
    pechersky committed Jan 7, 2022
    Copy the full SHA
    9d566aa View commit details
    Browse the repository at this point in the history

Commits on Jan 8, 2022

  1. Merge branch 'master' into pechersky/coe-laurent-poly-again

    @pechersky
    pechersky committed Jan 8, 2022
    Copy the full SHA
    c5a7a98 View commit details
    Browse the repository at this point in the history

  2. suggestion and cleaning, slay simp loop

    @pechersky
    pechersky committed Jan 8, 2022
    Copy the full SHA
    c48082c View commit details
    Browse the repository at this point in the history

  3. chore(ring_theory/laurent): more coe lemmas 

    And actually the changes reported in #11295
    @pechersky
    pechersky committed Jan 8, 2022
    Copy the full SHA
    5573bb2 View commit details
    Browse the repository at this point in the history

Commits on Jan 9, 2022

  1. Merge branch 'master' into pechersky/ratfunc-inj-laurent-series

    @pechersky
    pechersky committed Jan 9, 2022
    Copy the full SHA
    7402584 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'pechersky/coe-laurent-poly-again' into pechersky/ratfun… 

    …c-inj-laurent-series
    @pechersky
    pechersky committed Jan 9, 2022
    Copy the full SHA
    85252f2 View commit details
    Browse the repository at this point in the history

Commits on Jan 12, 2022

  1. Merge branch 'master' into pechersky/ratfunc-inj-laurent-series

    @pechersky
    pechersky committed Jan 12, 2022
    Copy the full SHA
    4c93e9d View commit details
    Browse the repository at this point in the history

  2. remove unmerged hom iffs

    @pechersky
    pechersky committed Jan 12, 2022
    Copy the full SHA
    68cc825 View commit details
    Browse the repository at this point in the history

  3. fix up lemma names 

    add TODO about coe_smul
    @pechersky
    pechersky committed Jan 12, 2022
    Copy the full SHA
    27e4f23 View commit details
    Browse the repository at this point in the history

Commits on Jan 22, 2022

  1. linting

    @pechersky
    pechersky committed Jan 22, 2022
    Copy the full SHA
    5eaef18 View commit details
    Browse the repository at this point in the history

Commits on Jan 26, 2022

  1. Merge branch 'master' into pechersky/ratfunc-inj-laurent-series

    @pechersky
    pechersky committed Jan 26, 2022
    Copy the full SHA
    094cc1e View commit details
    Browse the repository at this point in the history

  2. provide by suggestions

    @pechersky
    pechersky committed Jan 26, 2022
    Copy the full SHA
    32f15e8 View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2022

  1. finish coe_alg_hom, not coe_smul

    @pechersky
    pechersky committed Jan 27, 2022
    Copy the full SHA
    69c9275 View commit details
    Browse the repository at this point in the history

Commits on Jan 28, 2022

  1. linting

    @pechersky
    pechersky committed Jan 28, 2022
    Copy the full SHA
    d2d2523 View commit details
    Browse the repository at this point in the history

  2. Add docstring, is_scalar_tower

    @pechersky
    pechersky committed Jan 28, 2022
    Copy the full SHA
    592090f View commit details
    Browse the repository at this point in the history