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] - refactor(field_theory/is_alg_closed/basic): Generalize alg closures to commutative rings #11703

Closed
wants to merge 47 commits into from
Closed

[Merged by Bors] - refactor(field_theory/is_alg_closed/basic): Generalize alg closures to commutative rings #11703

wants to merge 47 commits into from

Commits on Sep 28, 2021

  1. start trying to generalize alg_losure to comm_ring

    @ChrisHughes24
    ChrisHughes24 committed Sep 28, 2021
    Configuration menu
    Copy the full SHA
    f2641dc View commit details
    Browse the repository at this point in the history

  2. start generalizing alg_closure

    @ChrisHughes24
    ChrisHughes24 committed Sep 28, 2021
    Configuration menu
    Copy the full SHA
    e8bf8b8 View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2021

  1. undo changes to lift

    @ChrisHughes24
    ChrisHughes24 committed Oct 3, 2021
    Configuration menu
    Copy the full SHA
    fc06120 View commit details
    Browse the repository at this point in the history

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

    @ChrisHughes24
    ChrisHughes24 committed Oct 3, 2021
    Configuration menu
    Copy the full SHA
    237d12d View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2021

  1. start on lift'

    @ChrisHughes24
    ChrisHughes24 committed Oct 4, 2021
    Configuration menu
    Copy the full SHA
    2a1d3d2 View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2022

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

    chughes committed Jan 27, 2022
    Configuration menu
    Copy the full SHA
    4c18e7e View commit details
    Browse the repository at this point in the history

  2. try to fix proof of lift'

    chughes committed Jan 27, 2022
    Configuration menu
    Copy the full SHA
    75a18ed View commit details
    Browse the repository at this point in the history

  3. prove lift' with sorries

    chughes committed Jan 27, 2022
    Configuration menu
    Copy the full SHA
    7f78a6a View commit details
    Browse the repository at this point in the history

  4. delete #print

    chughes committed Jan 27, 2022
    Configuration menu
    Copy the full SHA
    88885b1 View commit details
    Browse the repository at this point in the history

Commits on Jan 28, 2022

  1. feat(data/polynomial/reverse): lemmas about evaluating reversed polyn… 

    …omial
    chughes committed Jan 28, 2022
    Configuration menu
    Copy the full SHA
    b656bdb View commit details
    Browse the repository at this point in the history

  2. use invertible to state lemmas

    chughes committed Jan 28, 2022
    Configuration menu
    Copy the full SHA
    ca89e4d View commit details
    Browse the repository at this point in the history

  3. more lemmas

    chughes committed Jan 28, 2022
    Configuration menu
    Copy the full SHA
    b12c726 View commit details
    Browse the repository at this point in the history

  4. swap direction

    chughes committed Jan 28, 2022
    Configuration menu
    Copy the full SHA
    a3efe06 View commit details
    Browse the repository at this point in the history

  5. start work

    chughes committed Jan 28, 2022
    Configuration menu
    Copy the full SHA
    ee54769 View commit details
    Browse the repository at this point in the history

  6. chore(ring_theory/ocalization) weaken hypothesis from field to comm_ring 

    also making `B` an explicit argument
    @ChrisHughes24
    ChrisHughes24 committed Jan 28, 2022
    Configuration menu
    Copy the full SHA
    1a3c767 View commit details
    Browse the repository at this point in the history

  7. almost finish proof

    chughes committed Jan 28, 2022
    Configuration menu
    Copy the full SHA
    8d38cb5 View commit details
    Browse the repository at this point in the history

  8. Merge remote-tracking branch 'origin/master' into fraction_ring_algeb… 

    …raic
    chughes committed Jan 28, 2022
    Configuration menu
    Copy the full SHA
    ee57e20 View commit details
    Browse the repository at this point in the history

  9. fix build

    chughes committed Jan 28, 2022
    Configuration menu
    Copy the full SHA
    c5a41da View commit details
    Browse the repository at this point in the history

  10. fix build

    chughes committed Jan 28, 2022
    Configuration menu
    Copy the full SHA
    9b0ab7b View commit details
    Browse the repository at this point in the history

Commits on Jan 29, 2022

  1. almost finish proof

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    8a22777 View commit details
    Browse the repository at this point in the history

  2. fix build

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    a66869c View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/ChrisHughes24-patch-2' into frac… 

    …tion_ring_algebraic
    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    98433f3 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into fraction_ring_algeb… 

    …raic
    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    dfaa923 View commit details
    Browse the repository at this point in the history

  5. lint fix

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    87b63a1 View commit details
    Browse the repository at this point in the history

  6. finish proof

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    0cbd387 View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'origin/ChrisHughes24-patch-2' into frac… 

    …tion_ring_algebraic
    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    7a6f065 View commit details
    Browse the repository at this point in the history

  8. fix build

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    55309ac View commit details
    Browse the repository at this point in the history

  9. Merge remote-tracking branch 'origin/ChrisHughes24-patch-2' into frac… 

    …tion_ring_algebraic
    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    b4e1285 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'fraction_ring_algebraic' into generalize_alg_closure

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    26f71fe View commit details
    Browse the repository at this point in the history

  11. finish proof

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    2bf6f1c View commit details
    Browse the repository at this point in the history

  12. comment

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    a2b3557 View commit details
    Browse the repository at this point in the history

  13. fix build and lint

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    45b3fcc View commit details
    Browse the repository at this point in the history

  14. Merge branch 'fraction_ring_algebraic' into generalize_alg_closure

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    437b661 View commit details
    Browse the repository at this point in the history

  15. fix build

    chughes committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    70d1906 View commit details
    Browse the repository at this point in the history

Commits on Jan 30, 2022

  1. lint fix

    chughes committed Jan 30, 2022
    Configuration menu
    Copy the full SHA
    165fb44 View commit details
    Browse the repository at this point in the history

  2. delete #lint

    chughes committed Jan 30, 2022
    Configuration menu
    Copy the full SHA
    7fafeb1 View commit details
    Browse the repository at this point in the history

Commits on Jan 31, 2022

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

    chughes committed Jan 31, 2022
    Configuration menu
    Copy the full SHA
    12d18ec View commit details
    Browse the repository at this point in the history

Commits on Feb 1, 2022

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

    chughes committed Feb 1, 2022
    Configuration menu
    Copy the full SHA
    b5d08af View commit details
    Browse the repository at this point in the history

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

    chughes committed Feb 1, 2022
    Configuration menu
    Copy the full SHA
    eec68cf View commit details
    Browse the repository at this point in the history

  3. use no_zero_smul_divisors

    chughes committed Feb 1, 2022
    Configuration menu
    Copy the full SHA
    5aa4131 View commit details
    Browse the repository at this point in the history

  4. fix build

    chughes committed Feb 1, 2022
    Configuration menu
    Copy the full SHA
    855ee4e View commit details
    Browse the repository at this point in the history

Commits on Feb 2, 2022

  1. Update src/field_theory/is_alg_closed/basic.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @ChrisHughes24 @jcommelin
    ChrisHughes24 and jcommelin committed Feb 2, 2022
    Configuration menu
    Copy the full SHA
    c1f7568 View commit details
    Browse the repository at this point in the history

  2. Update src/field_theory/is_alg_closed/basic.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @ChrisHughes24 @jcommelin
    ChrisHughes24 and jcommelin committed Feb 2, 2022
    Configuration menu
    Copy the full SHA
    908d4a9 View commit details
    Browse the repository at this point in the history

  3. Update src/field_theory/is_alg_closed/basic.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @ChrisHughes24 @jcommelin
    ChrisHughes24 and jcommelin committed Feb 2, 2022
    Configuration menu
    Copy the full SHA
    12fedba View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into generalize_alg_closure

    chughes committed Feb 2, 2022
    Configuration menu
    Copy the full SHA
    4c9e0fc View commit details
    Browse the repository at this point in the history

  5. line length

    chughes committed Feb 2, 2022
    Configuration menu
    Copy the full SHA
    9216f3c View commit details
    Browse the repository at this point in the history

  6. line length

    chughes committed Feb 2, 2022
    Configuration menu
    Copy the full SHA
    a3873f2 View commit details
    Browse the repository at this point in the history